DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2021.19

A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus

Authors: Yannick Forster, Fabian Kunze, Gert Smolka, and Maximilian Wuttke

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract

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.

Cite as

Yannick Forster, Fabian Kunze, Gert Smolka, and Maximilian Wuttke. A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.ITP.2021.19,
  author =	{Forster, Yannick and Kunze, Fabian and Smolka, Gert and Wuttke, Maximilian},
  title =	{{A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value \lambda-Calculus}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{19:1--19:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.19},
  URN =		{urn:nbn:de:0030-drops-139142},
  doi =		{10.4230/LIPIcs.ITP.2021.19},
  annote =	{Keywords: formalizations of computational models, computability theory, Coq, time complexity, Turing machines, lambda calculus, Hoare logic}
}

Search Results

Documents authored by Wuttke, Maximilian

A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus

Abstract

Cite as

Thanks for your feedback!

Could not send message