Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)
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)
@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} }
Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
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)
@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} }
Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
Dominik Kirst and Benjamin Peters. Gödel’s Theorem Without Tears - Essential Incompleteness in Synthetic Computability. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{kirst_et_al:LIPIcs.CSL.2023.30, author = {Kirst, Dominik and Peters, Benjamin}, title = {{G\"{o}del’s Theorem Without Tears - Essential Incompleteness in Synthetic Computability}}, booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)}, pages = {30:1--30:18}, 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.30}, URN = {urn:nbn:de:0030-drops-174911}, doi = {10.4230/LIPIcs.CSL.2023.30}, annote = {Keywords: incompleteness, undecidability, synthetic computability theory} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
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)
@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} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Johannes Hostert, Andrej Dudenhefner, and Dominik Kirst. Undecidability of Dyadic First-Order Logic in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{hostert_et_al:LIPIcs.ITP.2022.19, author = {Hostert, Johannes and Dudenhefner, Andrej and Kirst, Dominik}, title = {{Undecidability of Dyadic First-Order Logic in Coq}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {19:1--19: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.19}, URN = {urn:nbn:de:0030-drops-167280}, doi = {10.4230/LIPIcs.ITP.2022.19}, annote = {Keywords: undecidability, synthetic computability, first-order logic, Coq} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Dominik Kirst. Computational Back-And-Forth Arguments in Constructive Type Theory. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 22:1-22:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{kirst:LIPIcs.ITP.2022.22, author = {Kirst, Dominik}, title = {{Computational Back-And-Forth Arguments in Constructive Type Theory}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {22:1--22:12}, 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.22}, URN = {urn:nbn:de:0030-drops-167311}, doi = {10.4230/LIPIcs.ITP.2022.22}, annote = {Keywords: back-and-forth method, computable isomorphisms, Coq} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Marc Hermes and Dominik Kirst. An Analysis of Tennenbaum’s Theorem in Constructive Type Theory. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{hermes_et_al:LIPIcs.FSCD.2022.9, author = {Hermes, Marc and Kirst, Dominik}, title = {{An Analysis of Tennenbaum’s Theorem in Constructive Type Theory}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {9:1--9:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-233-4}, ISSN = {1868-8969}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.9}, URN = {urn:nbn:de:0030-drops-162909}, doi = {10.4230/LIPIcs.FSCD.2022.9}, annote = {Keywords: first-order logic, Peano arithmetic, Tennenbaum’s theorem, constructive type theory, Church’s thesis, synthetic computability, Coq} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
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)
@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} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
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)
@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} }
Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
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)
@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} }
Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
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)
@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} }
Feedback for Dagstuhl Publishing