Demo Paper: Coqlex, an approach to generate verified lexers
| Autor: | Ouedraogo, Wendlasida, Ilik, Danko, Strassburger, Lutz |
|---|---|
| Přispěvatelé: | Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion (PARTOUT), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Siemens Mobility, Straßburger, Lutz |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: | |
| Zdroj: | ML 2021-ACM SIGPLAN Workshop on ML ML 2021-ACM SIGPLAN Workshop on ML, Aug 2021, Online event, United States |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|