Search Results

Documents authored by Smolka, Gert

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}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.21
Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga

Authors: Jonas Kaiser, Brigitte Pientka, and Gert Smolka

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
We give three formalisations of a proof of the equivalence of the usual, two-sorted presentation of System F and its single-sorted pure type system (PTS) variant Lambda2. This is established by reducing the typability problem of F to Lambda2 and vice versa. A key challenge is the treatment of variable binding and contextual information. The formalisations all share the same high level proof structure using relations to connect the type systems. They do, however, differ significantly in their representation and manipulation of variables and contextual information. In Coq, we use pure de Bruijn indices and parallel substitutions. In Abella, we use higher-order abstract syntax (HOAS) and nominal constants of the ambient reasoning logic. In Beluga, we also use HOAS but within contextual modal type theory. Our contribution is twofold. First, we present and compare a collection of machine-checked solutions to a non-trivial theoretical result. Second, we propose our proof as a benchmark, complementing the POPLmark and ORBI challenges by testing how well a given proof assistant or framework handles complex contextual information involving multiple type systems.
Cite as

Jonas Kaiser, Brigitte Pientka, and Gert Smolka. Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kaiser_et_al:LIPIcs.FSCD.2017.21,
  author =	{Kaiser, Jonas and Pientka, Brigitte and Smolka, Gert},
  title =	{{Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{21:1--21:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.21},
  URN =		{urn:nbn:de:0030-drops-77248},
  doi =		{10.4230/LIPIcs.FSCD.2017.21},
  annote =	{Keywords: Pure Type Systems, System F, de Bruijn Syntax, Higher-Order Abstract Syntax, Contextual Reasoning}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.271
Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification

Authors: Gert Smolka and Tobias Tebbi

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
A recursion scheme is an orthogonal rewriting system with rules of the form f(x1,...,xn) -> s. We consider terms to be equivalent if they rewrite to the same redex-free possibly infinite term after infinitary rewriting. For the restriction to the nonnested case, where nested redexes are forbidden, we prove the existence of principal unifiers modulo scheme equivalence. We give an algorithm computing principal unifiers by reducing the problem to a novel fragment of semi-unification we call anchored semi-unification. For anchored semi-unification, we develop a decision algorithm that returns a principal semi-unifier in the positive case.
Cite as

Gert Smolka and Tobias Tebbi. Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 271-286, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{smolka_et_al:LIPIcs.RTA.2013.271,
  author =	{Smolka, Gert and Tebbi, Tobias},
  title =	{{Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{271--286},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.271},
  URN =		{urn:nbn:de:0030-drops-40674},
  doi =		{10.4230/LIPIcs.RTA.2013.271},
  annote =	{Keywords: recursion schemes, semi-unification, infinitary rewriting}
}
Document
DOI: 10.4230/DagSemRep.24
Theorem Proving and Logic Programming with Constraints (Dagstuhl Seminar 9143)

Authors: Hubert Comon, Harald Ganzinger, Claude Kirchner, Hélène Kirchner, Jean-Louis Lassez, and Gert Smolka

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Hubert Comon, Harald Ganzinger, Claude Kirchner, Hélène Kirchner, Jean-Louis Lassez, and Gert Smolka. Theorem Proving and Logic Programming with Constraints (Dagstuhl Seminar 9143). Dagstuhl Seminar Report 24, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1992)

Copy BibTex To Clipboard

@TechReport{comon_et_al:DagSemRep.24,
  author =	{Comon, Hubert and Ganzinger, Harald and Kirchner, Claude and Kirchner, H\'{e}l\`{e}ne and Lassez, Jean-Louis and Smolka, Gert},
  title =	{{Theorem Proving and Logic Programming with Constraints (Dagstuhl Seminar 9143)}},
  pages =	{1--24},
  ISSN =	{1619-0203},
  year =	{1992},
  type = 	{Dagstuhl Seminar Report},
  number =	{24},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.24},
  URN =		{urn:nbn:de:0030-drops-149127},
  doi =		{10.4230/DagSemRep.24},
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact