Towards certified meta-programming with typed Template-Coq

DOI10.1007/978-3-319-94821-8_2MaRDI QIDQ1791140zbMATH OpenOpenAlexFDO

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

Publication date 4 October 2018

Copyright license Creative Commons Attribution 4.0 International

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)

Recommendations

• The \textsc{MetaCoq} project
• Mtac: a monad for typed tactic programming in Coq
• Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}
• Mtac: a monad for typed tactic programming in Coq
• scientific article; zbMATH DE number 1696760

Cited in

(8)

• Proof-producing synthesis of CakeML from monadic HOL functions
• The \textsc{MetaCoq} project
• \texttt{slepice}: towards a verified implementation of type theory in type theory
• scientific article; zbMATH DE number 5652621 (Why is no real title available?)
• Template-Coq
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}
• Extracting functional programs from Coq, in Coq

Describes a project that uses

Uses Software

• Gallina
• CertiCoq
• Mtac
• Coq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1791140)