A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus.

Yannick Forster, Fabian Kunze

Browse the full ITP paper archive.