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

The Coq code extraction feature produces executable code in conventional functional languages that can be integrated with existing components. Currently, Coq features extraction into OCaml, Haskell and Scheme. Many new target languages are not covered by the standard Coq extraction, such as languages for smart contracts and web development. Moreover, the extraction procedure is written in OCaml and is not verified. Implementing extraction in Coq itself allows for verification of the extraction process. We implement an extraction pipeline by extending the MetaCoq verified erasure with proof-generating passes and verified optimisations. We support several languages from the ML family in our pipeline: two languages for smart contracts (Liquidity and CameLIGO) and the Elm programming language. Our experience shows the pipeline can handle practical use cases and can be extended with more target languages including the ML family.

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