A certifying extraction with time bounds from Coq to call-by-value \lambda-calculus

DOI10.4230/LIPICS.ITP.2019.17MaRDI QIDQ5875425zbMATH OpenOpenAlexFDO

Authors Yannick Forster, Fabian Kunze

Publication date 3 February 2023

Full work available at URL https://arxiv.org/abs/1904.11818

zbMATH Keywords

\(\lambda\) calculuscall-by-valuecomputabilityconstructive type theoryCoqextraction

Mathematics Subject Classification ID

Cited in

(6)

• The \textsc{MetaCoq} project
• scientific article; zbMATH DE number 7566048 (Why is no real title available?)
• scientific article; zbMATH DE number 7566073 (Why is no real title available?)
• Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version)
• Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version
• Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}

Describes a project that uses

Uses Software

• Template-Coq
• OEuf
• CertiCoq
• Coq

This page was built for publication: A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus

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