2026-07-26T17:25:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13914 2024-03-06T10:53:07Z ddc:004 open_access

A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus Forster, Yannick Kunze, Fabian Smolka, Gert Wuttke, Maximilian formalizations of computational models computability theory Coq time complexity Turing machines lambda calculus Hoare logic The weak call-by-value λ-calculus Łand Turing machines can simulate each other with a polynomial overhead in time. This time invariance thesis for L, where the number of β-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 Ł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 Łand Turing machines, which we contribute to the Coq Library of Undecidability Proofs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yannick Forster and Fabian Kunze and Gert Smolka and Maximilian Wuttke 2021 Is Part Of LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2021.19 urn:nbn:de:0030-drops-139142 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.19 eng https://creativecommons.org/licenses/by/4.0/legalcode