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.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 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Dominique Larchey-Wendling and Jean-François Monin. Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{larcheywendling_et_al:LIPIcs.ITP.2023.21, author = {Larchey-Wendling, Dominique and Monin, Jean-Fran\c{c}ois}, title = {{Proof Pearl: Faithful Computation and Extraction of \mu-Recursive Algorithms in Coq}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {21:1--21:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.21}, URN = {urn:nbn:de:0030-drops-183963}, doi = {10.4230/LIPIcs.ITP.2023.21}, annote = {Keywords: Unbounded linear search, \mu-recursive functions, computational contents, Coq, extraction, OCaml} }
Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
Dominique Larchey-Wendling. Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{larcheywendling:LIPIcs.FSCD.2021.18, author = {Larchey-Wendling, Dominique}, title = {{Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq}}, booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)}, pages = {18:1--18:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-191-7}, ISSN = {1868-8969}, year = {2021}, volume = {195}, editor = {Kobayashi, Naoki}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.18}, URN = {urn:nbn:de:0030-drops-142568}, doi = {10.4230/LIPIcs.FSCD.2021.18}, annote = {Keywords: Undecidability, computability theory, many-one reduction, Minsky machines, Fractran, sub-exponential linear logic, 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} }