This is a static copy: The framework itself is now part of the Coq Library of Undecidability Proofs.

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

Yannick Forster [email protected], Fabian Kunze [email protected],

This repository contains the Coq formalisation of the ITP 2019 paper A certifying extraction with time bounds from Coq to call-by-value λ-calculus.

How to compile the code

git clone https://github.com/uds-psl/certifying-extraction-with-time-bounds.git
cd certifying-extraction-with-time-bounds
git submodule init
git submodule update
make -j 5

The files are tested to compile with The Coq Proof Assistant, version 8.8.2 (February 2019).

The compiled HTML version of the files can be found here or in the docs/website subdirectory of this repository.