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.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 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.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 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
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)
@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.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} }
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.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.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.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.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} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
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)
@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} }
Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
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)
@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} }
Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)
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)
@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}, }
Feedback for Dagstuhl Publishing