COPLAS: Annenkov, Extracting functional programs from Coq, in Coq
On 15 September, Danil Annenkov, Aarhus University, will give a COPLAS talk about code extraction.
Abstract
Many proof assistants offer a possibility for obtaining code in a conventional functional programming language from formalized developments. This functionality is called code extraction. The Coq proof assistant supports extraction to OCaml, Haskell, and Scheme out of the box. However, the extraction functionality itself is not verified. Moreover, there are many interesting target languages not covered by the standard extraction. We address these challenges by developing an extraction pipeline entirely in Coq by extending the MetaCoq verified erasure procedure. We also develop pretty-printing functionality for new target languages: Elm, Rust, Liquidity, and CameLIGO. In total, this gives us a way to write dependently typed programs in Coq, verify, and extract them to several target languages while retaining a small trusted computing base.
In this talk, we present the current status of our development, motivate the transformations we currently have in the pipeline and discuss further opportunities for extending the pipeline with new target languages.
Joint work with Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters.
Bio
Danil Annenkov is a postdoc researcher at the Concordium Blockchain Research Center, Aarhus University working on formal verification of smart contracts. His research areas include programming language semantics, formal verification, proof assistants, and type theory. Danil Annenkov received his PhD degree in Computer Science from the University of Copenhagen, DIKU in 2018 under the supervision of Martin Elsman. After receiving his PhD degree, Annenkov was a postdoc researcher at INRIA Nantes, France, where he worked on extending the Coq proof assistant with new reasoning principles.
Registration
All are welcome. No registration required.
Host: Martin Elsman
You can subscribe to the COPLAS talks here to get more information.