A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value λ-Calculus
(pdf)
Yannick Forster, Fabian Kunze, Gert Smolka, Maximilian Wuttke
12th International Conference on Interactive Theorem Proving (ITP 2021)
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq
(pdf)
Lennard Gäher, Fabian Kunze
12th International Conference on Interactive Theorem Proving (ITP 2021)
Verified Programming of Turing Machines in Coq
(pdf)
Yannick Forster, Fabian Kunze, Maximilian Wuttke
9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20–21, 2020
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
(pdf)
Yannick Forster, Fabian Kunze, Marc Roth
47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020), New Orleans, USA
A certifying extraction with time bounds from Coq to call-by-value λ-calculus
(pdf)
Yannick Forster, Fabian Kunze
Interactive Theorem Proving - 10th International Conference, ITP 2019, Portland, USA
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
(pdf)
Fabian Kunze, Gert Smolka, Yannick Forster
16th Asian Symposium on Programming Languages and Systems, APLAS 2018, Wellington, New Zealand, December 2-6