From 5e95cc064ad12661029d0c645ae86b101f74df97 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 27 Sep 2019 18:26:10 +0200 Subject: [PATCH] Add extraction with time bounds reference in the Papers section --- README.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index b9a267e88..b9bbf70d6 100644 --- a/README.md +++ b/README.md @@ -153,7 +153,12 @@ Papers - ["Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq"](https://www.irif.fr/~sozeau/research/publications/drafts/Coq_Coq_Correct.pdf). Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau and Théo Winterhalter. Submitted, July 2019. - + +- [A certifying extraction with time bounds from Coq to call-by-value λ-calculus](https://www.ps.uni-saarland.de/Publications/documents/ForsterKunze_2019_Certifying-extraction.pdf). + Yannick Forster and Fabian Kunze. + ITP 2019. + [Example](https://github.com/uds-psl/certifying-extraction-with-time-bounds/blob/master/Tactics/Extract.v) + - ["The MetaCoq Project"](https://www.irif.fr/~sozeau/research/publications/drafts/The_MetaCoq_Project.pdf) Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau and Théo Winterhalter.