Coq Workshop talk: Verified Extraction from Coq to a Lambda-Calculus
By: Yannick Forster and Fabian Kunze
Advisor: Prof. Dr. Gert Smolka
Abstract
We present a framework to export programs in Coq to a weak call-by-value lambda calculus. The
calculus can be seen as a very basic functional programming language, featuring abstraction, match-
constructs based on Scott’s encoding and full recursion.
The extraction from Coq is not verified itself, but produces proofs for the correctness of each single
extracted program semi-automatically. The frameworks builds on the Coq plugin Template Coq by
Gregory Malecha. It eliminates the non-computational parts of the Gallina program and produces a
lambda-term and the corresponding correctness statement, which in turn can be verified using several
provided automation tactics.
Attached Documents
Legal notice, Privacy policy
