Demo Paper: Coqlex, an approach to generate verified lexers - Archive ouverte HAL Access content directly
Conference Papers Year :

Demo Paper: Coqlex, an approach to generate verified lexers

(1, 2) , (2) , (1)
1
2

Abstract

A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of every component of the tool-chain. In order to contribute to the end-to-end verification of compilers, we implemented a verified lexer generator with usage similar to OCamllex. This software-Coqlex-reads a lexer specification and generates a lexer equipped with Coq proofs of its correctness. Although the performance of the generated lexers does not measure up to the performance of a standard lexer generator such as OCamllex, the safety guarantees it comes with make it an interesting alternative to use when implementing totally verified compilers or other language processing tools.
Fichier principal
Vignette du fichier
Demo_Paper.pdf (211.81 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03470713 , version 1 (08-12-2021)

Identifiers

  • HAL Id : hal-03470713 , version 1

Cite

Wendlasida Ouedraogo, Danko Ilik, Lutz Strassburger. Demo Paper: Coqlex, an approach to generate verified lexers. ML 2021-ACM SIGPLAN Workshop on ML, Aug 2021, Online event, United States. ⟨hal-03470713⟩
41 View
66 Download

Share

Gmail Facebook Twitter LinkedIn More