Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, Marijn J. H. Heule. EmptyHexagonLean (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@misc{dagstuhl-artifact-22467, title = {{EmptyHexagonLean}}, author = {Subercaseaux, Bernardo and Nawrocki, Wojciech and Gallicchio, James and Codel, Cayden and Carneiro, Mario and Heule, Marijn J. H.}, note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:29dc0e7145296997bcb1230b4e03cd14c8d75617;origin=https://github.com/bsubercaseaux/EmptyHexagonLean;visit=swh:1:snp:0e11d6564bd15317306605932e0acd87cf3d7f80;anchor=swh:1:rev:d7f798ffc8deabc2f3ca1ae36e92e0250e57c205}{\texttt{swh:1:dir:29dc0e7145296997bcb1230b4e03cd14c8d75617}} (visited on 2024-11-28)}, url = {https://github.com/bsubercaseaux/EmptyHexagonLean/tree/itp2024}, doi = {10.4230/artifacts.22467}, }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule. Formal Verification of the Empty Hexagon Number. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{subercaseaux_et_al:LIPIcs.ITP.2024.35, author = {Subercaseaux, Bernardo and Nawrocki, Wojciech and Gallicchio, James and Codel, Cayden and Carneiro, Mario and Heule, Marijn J. H.}, title = {{Formal Verification of the Empty Hexagon Number}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {35:1--35:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.35}, URN = {urn:nbn:de:0030-drops-207633}, doi = {10.4230/LIPIcs.ITP.2024.35}, annote = {Keywords: Empty Hexagon Number, Discrete Computational Geometry, Erd\H{o}s-Szekeres} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Mario Carneiro, Chad E. Brown, and Josef Urban. Automated Theorem Proving for Metamath. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{carneiro_et_al:LIPIcs.ITP.2023.9, author = {Carneiro, Mario and Brown, Chad E. and Urban, Josef}, title = {{Automated Theorem Proving for Metamath}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {9:1--9:19}, 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.9}, URN = {urn:nbn:de:0030-drops-183846}, doi = {10.4230/LIPIcs.ITP.2023.9}, annote = {Keywords: Metamath, Automated theorem proving, Interactive theorem proving, Formal proof assistants, proof discovery} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Mario Carneiro. Reimplementing Mizar in Rust. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{carneiro:LIPIcs.ITP.2023.10, author = {Carneiro, Mario}, title = {{Reimplementing Mizar in Rust}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {10:1--10:18}, 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.10}, URN = {urn:nbn:de:0030-drops-183852}, doi = {10.4230/LIPIcs.ITP.2023.10}, annote = {Keywords: Mizar, proof checker, software, Rust} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Jeremy Avigad, Mario Carneiro, and Simon Hudon. Data Types as Quotients of Polynomial Functors. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{avigad_et_al:LIPIcs.ITP.2019.6, author = {Avigad, Jeremy and Carneiro, Mario and Hudon, Simon}, title = {{Data Types as Quotients of Polynomial Functors}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {6:1--6:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.6}, URN = {urn:nbn:de:0030-drops-110612}, doi = {10.4230/LIPIcs.ITP.2019.6}, annote = {Keywords: data types, polynomial functors, inductive types, coinductive types} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Mario Carneiro. Formalizing Computability Theory via Partial Recursive Functions. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{carneiro:LIPIcs.ITP.2019.12, author = {Carneiro, Mario}, title = {{Formalizing Computability Theory via Partial Recursive Functions}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {12:1--12:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.12}, URN = {urn:nbn:de:0030-drops-110671}, doi = {10.4230/LIPIcs.ITP.2019.12}, annote = {Keywords: Lean, computability, halting problem, primitive recursion} }
Feedback for Dagstuhl Publishing