Demo Paper : Coqlex, an approach to generate verified lexers
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.
Thu 26 AugDisplayed time zone: Seoul change
20:00 - 21:30
|Formalizing OCaml GADT typing in Coq|
MLPre-print File Attached
|Demo Paper : Coqlex, an approach to generate verified lexers|
Wendlasida Ouedraogo Siemens Mobility & Inria Saclay, Danko Ilik Siemens Mobility, Lutz Strassburger Inria Saclay & LIX, Ecole PolytechniqueMedia Attached File Attached
|Code Extraction from Coq to ML-like languages|
Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University, Bas Spitters Aarhus UniversityLink to publication File Attached