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.
submitted_paper (Demo_Paper.pdf) | 211KiB |
slides (Coqlex.pptx) | 4.22MiB |
Thu 26 AugDisplayed time zone: Seoul change
20:00 - 21:30 | |||
20:00 30mTalk | Formalizing OCaml GADT typing in Coq ML Pre-print File Attached | ||
20:30 30mTalk | Demo Paper : Coqlex, an approach to generate verified lexers ML Wendlasida Ouedraogo Siemens Mobility & Inria Saclay, Danko Ilik Siemens Mobility, Lutz Strassburger Inria Saclay & LIX, Ecole Polytechnique Media Attached File Attached | ||
21:00 30mTalk | Code Extraction from Coq to ML-like languages ML Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University, Bas Spitters Aarhus University Link to publication File Attached |