11 Search Results for "Smolka, Gert"

Document
DOI: 10.4230/LIPIcs.CSL.2024.29
The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions

Authors: Yannick Forster, Dominik Kirst, and Niklas Mück

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
The Kleene-Post theorem and Post’s theorem are two central and historically important results in the development of oracle computability theory, clarifying the structure of Turing reducibility degrees. They state, respectively, that there are incomparable Turing degrees and that the arithmetical hierarchy is connected to the relativised form of the halting problem defined via Turing jumps. We study these two results in the calculus of inductive constructions (CIC), the constructive type theory underlying the Coq proof assistant. CIC constitutes an ideal foundation for the formalisation of computability theory for two reasons: First, like in other constructive foundations, computable functions can be treated via axioms as a purely synthetic notion rather than being defined in terms of a concrete analytic model of computation such as Turing machines. Furthermore and uniquely, CIC allows consistently assuming classical logic via the law of excluded middle or weaker variants on top of axioms for synthetic computability, enabling both fully classical developments and taking the perspective of constructive reverse mathematics on computability theory. In the present paper, we give a fully constructive construction of two Turing-incomparable degrees à la Kleene-Post and observe that the classical content of Post’s theorem seems to be related to the arithmetical hierarchy of the law of excluded middle due to Akama et. al. Technically, we base our investigation on a previously studied notion of synthetic oracle computability and contribute the first consistency proof of a suitable enumeration axiom. All results discussed in the paper are mechanised and contributed to the Coq library of synthetic computability.
Cite as

Yannick Forster, Dominik Kirst, and Niklas Mück. The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.CSL.2024.29,
  author =	{Forster, Yannick and Kirst, Dominik and M\"{u}ck, Niklas},
  title =	{{The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.29},
  URN =		{urn:nbn:de:0030-drops-196728},
  doi =		{10.4230/LIPIcs.CSL.2024.29},
  annote =	{Keywords: Constructive mathematics, Computability theory, Logical foundations, Constructive type theory, Interactive theorem proving, Coq proof assistant}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.21
Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq

Authors: Yannick Forster and Felix Jahn

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
We present a constructive analysis and machine-checked theory of one-one, many-one, and truth-table reductions based on synthetic computability theory in the Calculus of Inductive Constructions, the type theory underlying the proof assistant Coq. We give elegant, synthetic, and machine-checked proofs of Post’s landmark results that a simple predicate exists, is enumerable, undecidable, but many-one incomplete (Post’s problem for many-one reducibility), and a hypersimple predicate exists, is enumerable, undecidable, but truth-table incomplete (Post’s problem for truth-table reducibility). In synthetic computability, one assumes axioms allowing to carry out computability theory with all definitions and proofs purely in terms of functions of the type theory with no mention of a model of computation. Proofs can focus on the essence of the argument, without having to sacrifice formality. Synthetic computability also clears the lense for constructivisation. Our constructively careful definition of simple and hypersimple predicates allows us to not assume classical axioms, not even Markov’s principle, still yielding the expected strong results.
Cite as

Yannick Forster and Felix Jahn. Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.CSL.2023.21,
  author =	{Forster, Yannick and Jahn, Felix},
  title =	{{Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{21:1--21:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.21},
  URN =		{urn:nbn:de:0030-drops-174820},
  doi =		{10.4230/LIPIcs.CSL.2023.21},
  annote =	{Keywords: type theory, computability theory, constructive mathematics, Coq}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.12
Synthetic Kolmogorov Complexity in Coq

Authors: Yannick Forster, Fabian Kunze, and Nils Lauermann

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract
We present a generalised, constructive, and machine-checked approach to Kolmogorov complexity in the constructive type theory underlying the Coq proof assistant. By proving that nonrandom numbers form a simple predicate, we obtain elegant proofs of undecidability for random and nonrandom numbers and a proof of uncomputability of Kolmogorov complexity. We use a general and abstract definition of Kolmogorov complexity and subsequently instantiate it to several definitions frequently found in the literature. Whereas textbook treatments of Kolmogorov complexity usually rely heavily on classical logic and the axiom of choice, we put emphasis on the constructiveness of all our arguments, however without blurring their essence. We first give a high-level proof idea using classical logic, which can be formalised with Markov’s principle via folklore techniques we subsequently explain. Lastly, we show a strategy how to eliminate Markov’s principle from a certain class of computability proofs, rendering all our results fully constructive. All our results are machine-checked by the Coq proof assistant, which is enabled by using a synthetic approach to computability: rather than formalising a model of computation, which is well known to introduce a considerable overhead, we abstractly assume a universal function, allowing the proofs to focus on the mathematical essence.
Cite as

Yannick Forster, Fabian Kunze, and Nils Lauermann. Synthetic Kolmogorov Complexity in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.ITP.2022.12,
  author =	{Forster, Yannick and Kunze, Fabian and Lauermann, Nils},
  title =	{{Synthetic Kolmogorov Complexity in Coq}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.12},
  URN =		{urn:nbn:de:0030-drops-167219},
  doi =		{10.4230/LIPIcs.ITP.2022.12},
  annote =	{Keywords: Kolmogorov complexity, computability theory, random numbers, constructive matemathics, synthetic computability theory, constructive type theory, Coq}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.18
Constructive Many-One Reduction from the Halting Problem to Semi-Unification

Authors: Andrej Dudenhefner

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
The undecidability of semi-unification (unification combined with matching) has been proven by Kfoury, Tiuryn, and Urzyczyn in the 1990s. The original argument is by Turing reduction from Turing machine immortality (existence of a diverging configuration). There are several aspects of the existing work which can be improved upon. First, many-one completeness of semi-unification is not established due to the use of Turing reductions. Second, existing mechanizations do not cover a comprehensive reduction from Turing machine halting to semi-unification. Third, reliance on principles such as König’s lemma or the fan theorem does not support constructivity of the arguments. Improving upon the above aspects, the present work gives a constructive many-one reduction from the Turing machine halting problem to semi-unification. This establishes many-one completeness of semi-unification. Computability of the reduction function, constructivity of the argument, and correctness of the argument is witnessed by an axiom-free mechanization in the Coq proof assistant. The mechanization is incorporated into the existing Coq library of undecidability proofs. Notably, the mechanization relies on a technique invented by Hooper in the 1960s for Turing machine immortality. An immediate consequence of the present work is an alternative approach to the constructive many-one equivalence of System F typability and System F type checking, compared to the argument established in the 1990s by Wells.
Cite as

Andrej Dudenhefner. Constructive Many-One Reduction from the Halting Problem to Semi-Unification. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dudenhefner:LIPIcs.CSL.2022.18,
  author =	{Dudenhefner, Andrej},
  title =	{{Constructive Many-One Reduction from the Halting Problem to Semi-Unification}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{18:1--18:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.18},
  URN =		{urn:nbn:de:0030-drops-157380},
  doi =		{10.4230/LIPIcs.CSL.2022.18},
  annote =	{Keywords: constructive mathematics, undecidability, mechanization, semi-unification}
}
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-dev.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.ITP.2021.23
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq

Authors: Dominik Kirst and Marc Hermes

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

Abstract
We mechanise the undecidability of various first-order axiom systems in Coq, employing the synthetic approach to computability underlying the growing Coq Library of Undecidability Proofs. Concretely, we cover both semantic and deductive entailment in fragments of Peano arithmetic (PA) and Zermelo-Fraenkel set theory (ZF), with their undecidability established by many-one reductions from solvability of Diophantine equations, i.e. Hilbert’s tenth problem (H10), and the Post correspondence problem (PCP), respectively. In the synthetic setting based on the computability of all functions definable in a constructive foundation, such as Coq’s type theory, it suffices to define these reductions as meta-level functions with no need for further encoding in a formalised model of computation. The concrete cases of PA and ZF are prepared by a general synthetic theory of undecidable axiomatisations, focusing on well-known connections to consistency and incompleteness. Specifically, our reductions rely on the existence of standard models, necessitating additional assumptions in the case of full ZF, and all axiomatic extensions still justified by such standard models are shown incomplete. As a by-product of the undecidability of ZF formulated using only membership and no equality symbol, we obtain the undecidability of first-order logic with a single binary relation.
Cite as

Dominik Kirst and Marc Hermes. Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kirst_et_al:LIPIcs.ITP.2021.23,
  author =	{Kirst, Dominik and Hermes, Marc},
  title =	{{Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{23:1--23: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.23},
  URN =		{urn:nbn:de:0030-drops-139188},
  doi =		{10.4230/LIPIcs.ITP.2021.23},
  annote =	{Keywords: undecidability, synthetic computability, first-order logic, incompleteness, Peano arithmetic, ZF set theory, constructive type theory, Coq}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.21
Church’s Thesis and Related Axioms in Coq’s Type Theory

Authors: Yannick Forster

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
"Church’s thesis" (CT) as an axiom in constructive logic states that every total function of type ℕ → ℕ is computable, i.e. definable in a model of computation. CT is inconsistent both in classical mathematics and in Brouwer’s intuitionism since it contradicts weak Kőnig’s lemma and the fan theorem, respectively. Recently, CT was proved consistent for (univalent) constructive type theory. Since neither weak Kőnig’s lemma nor the fan theorem is a consequence of just logical axioms or just choice-like axioms assumed in constructive logic, it seems likely that CT is inconsistent only with a combination of classical logic and choice axioms. We study consequences of CT and its relation to several classes of axioms in Coq’s type theory, a constructive type theory with a universe of propositions which proves neither classical logical axioms nor strong choice axioms. We thereby provide a partial answer to the question as to which axioms may preserve computational intuitions inherent to type theory, and which certainly do not. The paper can also be read as a broad survey of axioms in type theory, with all results mechanised in the Coq proof assistant.
Cite as

Yannick Forster. Church’s Thesis and Related Axioms in Coq’s Type Theory. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{forster:LIPIcs.CSL.2021.21,
  author =	{Forster, Yannick},
  title =	{{Church’s Thesis and Related Axioms in Coq’s Type Theory}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{21:1--21:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.21},
  URN =		{urn:nbn:de:0030-drops-134552},
  doi =		{10.4230/LIPIcs.CSL.2021.21},
  annote =	{Keywords: Church’s thesis, constructive type theory, constructive reverse mathematics, synthetic computability theory, Coq}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.27
Hilbert’s Tenth Problem in Coq

Authors: Dominique Larchey-Wendling and Yannick Forster

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq’s constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem - in our case by a Minsky machine - is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway’s FRACTRAN language as intermediate layer.
Cite as

Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 27:1-27:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{larcheywendling_et_al:LIPIcs.FSCD.2019.27,
  author =	{Larchey-Wendling, Dominique and Forster, Yannick},
  title =	{{Hilbert’s Tenth Problem in Coq}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{27:1--27:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.27},
  URN =		{urn:nbn:de:0030-drops-105342},
  doi =		{10.4230/LIPIcs.FSCD.2019.27},
  annote =	{Keywords: Hilbert’s tenth problem, Diophantine equations, undecidability, computability theory, reduction, Minsky machines, Fractran, Coq, type theory}
}
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-dev.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-dev.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-dev.dagstuhl.de/entities/document/10.4230/DagSemRep.24},
  URN =		{urn:nbn:de:0030-drops-149127},
  doi =		{10.4230/DagSemRep.24},
}
  • Refine by Author
  • 6 Forster, Yannick
  • 4 Smolka, Gert
  • 2 Kirst, Dominik
  • 2 Kunze, Fabian
  • 1 Comon, Hubert
  • Show More...

  • Refine by Classification
  • 7 Theory of computation → Type theory
  • 5 Theory of computation → Constructive mathematics
  • 2 Theory of computation → Computability
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Models of computation

  • Refine by Keyword
  • 6 Coq
  • 4 computability theory
  • 3 constructive type theory
  • 3 undecidability
  • 2 constructive mathematics
  • Show More...

  • Refine by Type
  • 11 document

  • Refine by Publication Year
  • 3 2021
  • 2 2022
  • 1 1992
  • 1 2013
  • 1 2017
  • Show More...

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