ICFP 2021
Sun 22 - Sat 28 August 2021
Thu 26 Aug 2021 20:30 - 21:00 at ML - Compiler & Language Correctness Chair(s): Robert Atkey

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 Aug

Displayed time zone: Seoul change

20:00 - 21:30
Compiler & Language CorrectnessML at ML
Chair(s): Robert Atkey University of Strathclyde
Formalizing OCaml GADT typing in Coq
Jacques Garrigue Nagoya University, Xuanrui Qi Nagoya University
Pre-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 Polytechnique
Media 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 University
Link to publication File Attached