Yannick Forster

Saarland University Computer Science

Research Immersion Lab: Verified Extraction from Coq to a Lambda-Calculus

Author: Yannick Forster, joint work with Fabian Kunze
Advisor: Prof. Dr. Gert Smolka


We present a framework to export programs in Coq to a weak call-by-value lambda calculus called L. L can be seen as a very basic functional programming language featuring abstraction, full recursion and match-constructs based on Scott's encoding.

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. It eliminates the non-computational parts of the Coq program and produces a term in L and the corresponding correctness statement, which in turn can be verified using several provided automation tactics.

Using the framework, one can focus on the interesting parts of developments in L, because the task of programming is taken care of. We use the framework to develop a formalization of Computability theory as a case study.

Attached Documents

Legal notice, Privacy policy