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)
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