Towards certified meta-programming with typed Template-Coq

DOI10.1007/978-3-319-94821-8_2zbMath1468.68071OpenAlexW2805888229MaRDI QIDQ1791140

Cyril Cohen, Nicolas Tabareau, Matthieu Sozeau, Abhishek Anand, Simon Boulier

Publication date: 4 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94821-8_2

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

Extracting functional programs from Coq, in Coq ⋮ Proof-producing synthesis of CakeML from monadic HOL functions ⋮ The \textsc{MetaCoq} project ⋮ Template-Coq ⋮ \texttt{slepice}: towards a verified implementation of type theory in type theory

Uses Software

• Coq
• Mtac
• CertiCoq
• Gallina

This page was built for publication: Towards certified meta-programming with typed Template-Coq