## Extracting functional programs from Coq, in Coq

Publikation: Working paper/Preprint PreprintForskning

### Standard

Extracting functional programs from Coq, in Coq. / Annenkov, Danil; Milo, Mikkel; Nielsen, Jakob Botsch; Spitters, Bas.

2021.

Publikation: Working paper/Preprint PreprintForskning

### Bibtex

@techreport{e53940c19b484c558462d0872659e097,
title = "Extracting functional programs from Coq, in Coq",
abstract = " We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. We extend the MetaCoq erasure output language with typing information and use it as an intermediate representation, which we call $\lambda^T_\square$. We complement the extraction functionality with a full pipeline that includes several standard transformations (eta-expansion, inlining, etc) implemented in a proof-generating manner along with a verified optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. From the optimised $\lambda^T_\square$ representation, we obtain code in two functional smart contract languages (Liquidity and CameLIGO), the functional language Elm, and a subset of the multi-paradigm language for systems programming Rust. Rust is currently gaining popularity as a language for smart contracts, and we demonstrate how our extraction can be used to extract smart contract code for the Concordium network. The development is done in the context of the ConCert framework that enables smart contract verification. We contribute with two verified real-world smart contracts (boardroom voting and escrow), which we use, among other examples, to exemplify the applicability of the pipeline. In addition, we develop a verified web application and extract it to fully functional Elm code. In total, this gives us a way to write dependently typed programs in Coq, verify, and then extract them to several target languages while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages. ",
keywords = "cs.PL, cs.LO",
author = "Danil Annenkov and Mikkel Milo and Nielsen, {Jakob Botsch} and Bas Spitters",
note = "57 pages; Coq development: https://github.com/AU-COBRA/ConCert/tree/journal-2021",
year = "2021",
month = aug,
day = "6",
language = "English",
type = "WorkingPaper",

}

### RIS

TY - UNPB

T1 - Extracting functional programs from Coq, in Coq

AU - Annenkov, Danil

AU - Milo, Mikkel

AU - Nielsen, Jakob Botsch

AU - Spitters, Bas

N1 - 57 pages; Coq development: https://github.com/AU-COBRA/ConCert/tree/journal-2021

PY - 2021/8/6

Y1 - 2021/8/6

N2 - We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. We extend the MetaCoq erasure output language with typing information and use it as an intermediate representation, which we call $\lambda^T_\square$. We complement the extraction functionality with a full pipeline that includes several standard transformations (eta-expansion, inlining, etc) implemented in a proof-generating manner along with a verified optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. From the optimised $\lambda^T_\square$ representation, we obtain code in two functional smart contract languages (Liquidity and CameLIGO), the functional language Elm, and a subset of the multi-paradigm language for systems programming Rust. Rust is currently gaining popularity as a language for smart contracts, and we demonstrate how our extraction can be used to extract smart contract code for the Concordium network. The development is done in the context of the ConCert framework that enables smart contract verification. We contribute with two verified real-world smart contracts (boardroom voting and escrow), which we use, among other examples, to exemplify the applicability of the pipeline. In addition, we develop a verified web application and extract it to fully functional Elm code. In total, this gives us a way to write dependently typed programs in Coq, verify, and then extract them to several target languages while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.

AB - We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. We extend the MetaCoq erasure output language with typing information and use it as an intermediate representation, which we call $\lambda^T_\square$. We complement the extraction functionality with a full pipeline that includes several standard transformations (eta-expansion, inlining, etc) implemented in a proof-generating manner along with a verified optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. From the optimised $\lambda^T_\square$ representation, we obtain code in two functional smart contract languages (Liquidity and CameLIGO), the functional language Elm, and a subset of the multi-paradigm language for systems programming Rust. Rust is currently gaining popularity as a language for smart contracts, and we demonstrate how our extraction can be used to extract smart contract code for the Concordium network. The development is done in the context of the ConCert framework that enables smart contract verification. We contribute with two verified real-world smart contracts (boardroom voting and escrow), which we use, among other examples, to exemplify the applicability of the pipeline. In addition, we develop a verified web application and extract it to fully functional Elm code. In total, this gives us a way to write dependently typed programs in Coq, verify, and then extract them to several target languages while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.

KW - cs.PL

KW - cs.LO

M3 - Preprint

BT - Extracting functional programs from Coq, in Coq

ER -