Publication details

Saarland University Computer Science

A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value λ-Calculus

Yannick Forster, Fabian Kunze, Gert Smolka, Maximilian Wuttke

12th International Conference on Interactive Theorem Proving (ITP 2021), pp. 19:1--19:20, Schloss Dagstuhl -Leibniz-Zentrum für Informatik, January 2021

The weak call-by-value lambda-calculus L and Turing machines can simulate each other with a polynomial overhead in time. This time invariance thesis for L, where the number of beta-reductions of a computation is taken as its time complexity, is the culmination of a 25-years line of research, combining work by Blelloch, Greiner, Dal Lago, Martini, Accattoli, Forster, Kunze, Roth, and Smolka. The present paper presents a mechanised proof of the time invariance thesis for L, constituting the first mechanised equivalence proof between two standard models of computation covering time complexity. The mechanisation builds on an existing framework for the extraction of Coq functions to L and contributes a novel Hoare logic framework for the verification of Turing machines.
The mechanised proof of the time invariance thesis establishes L as model for future developments of mechanised computational complexity theory regarding time. It can also be seen as a non-trivial but elementary case study of time-complexity-preserving translations between a functional language and a sequential machine model. As a by-product, we obtain a mechanised many-one equivalence proof of the halting problems for L and Turing machines, which we contribute to the Coq Library of Undecidability Proofs.

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy