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

DOI10.4230/LIPIcs.ITP.2019.17OpenAlexW4311008361MaRDI QIDQ5875425

Fabian Kunze, Yannick Forster

Publication date: 3 February 2023

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

zbMATH Keywords

constructive type theorycomputabilityCoqextractioncall-by-value\(\lambda\) calculus

Mathematics Subject Classification ID

Related Items (5)

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 ⋮ The \textsc{MetaCoq} project ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• Coq
• CertiCoq
• OEuf
• Template-Coq

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

 $\lambda$-calculus