Saarland University Computer Science

Coq Workshop talk: Verified Extraction from Coq to a Lambda-Calculus

By: Yannick Forster and Fabian Kunze
Advisor: Prof. Dr. Gert Smolka


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

Yannick Forster, Sat Aug 27 09:10:01 2016