14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 1-660, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@Proceedings{naumowicz_et_al:LIPIcs.ITP.2023, title = {{LIPIcs, Volume 268, ITP 2023, Complete Volume}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {1--660}, 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}, URN = {urn:nbn:de:0030-drops-183747}, doi = {10.4230/LIPIcs.ITP.2023}, annote = {Keywords: LIPIcs, Volume 268, ITP 2023, Complete Volume} }
14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{naumowicz_et_al:LIPIcs.ITP.2023.0, author = {Naumowicz, Adam and Thiemann, Ren\'{e}}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {0:i--0:x}, 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.0}, URN = {urn:nbn:de:0030-drops-183755}, doi = {10.4230/LIPIcs.ITP.2023.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Angeliki Koutsoukou-Argyraki. Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{koutsoukouargyraki:LIPIcs.ITP.2023.1, author = {Koutsoukou-Argyraki, Angeliki}, title = {{Formalisation of Additive Combinatorics in Isabelle/HOL}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {1:1--1:2}, 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.1}, URN = {urn:nbn:de:0030-drops-183760}, doi = {10.4230/LIPIcs.ITP.2023.1}, annote = {Keywords: Additive combinatorics, additive number theory, combinatorial number theory, formalisation of mathematics, interactive theorem proving, proof assistants, Isabelle/HOL} }
Robbert Krebbers. Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{krebbers:LIPIcs.ITP.2023.2, author = {Krebbers, Robbert}, title = {{Interactive and Automated Proofs in Modal Separation Logic}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {2:1--2:1}, 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.2}, URN = {urn:nbn:de:0030-drops-183770}, doi = {10.4230/LIPIcs.ITP.2023.2}, annote = {Keywords: Program Verification, Separation Logic, Step-Indexing, Modal Logic, Interactive Theorem Proving, Proof Automation, Iris, Coq} }
Mohammad Abdulaziz and Christoph Madlener. A Formal Analysis of RANKING. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{abdulaziz_et_al:LIPIcs.ITP.2023.3, author = {Abdulaziz, Mohammad and Madlener, Christoph}, title = {{A Formal Analysis of RANKING}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {3:1--3: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.3}, URN = {urn:nbn:de:0030-drops-183785}, doi = {10.4230/LIPIcs.ITP.2023.3}, annote = {Keywords: Matching Theory, Formalized Mathematics, Online Algorithms} }
Oskar Abrahamsson and Magnus O. Myreen. Fast, Verified Computation for Candle. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{abrahamsson_et_al:LIPIcs.ITP.2023.4, author = {Abrahamsson, Oskar and Myreen, Magnus O.}, title = {{Fast, Verified Computation for Candle}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {4:1--4: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.4}, URN = {urn:nbn:de:0030-drops-183797}, doi = {10.4230/LIPIcs.ITP.2023.4}, annote = {Keywords: Prover soundness, Higher-order logic, Interactive theorem proving} }
Beniamino Accattoli, Horace Blanc, and Claudio Sacerdoti Coen. Formalizing Functions as Processes. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{accattoli_et_al:LIPIcs.ITP.2023.5, author = {Accattoli, Beniamino and Blanc, Horace and Sacerdoti Coen, Claudio}, title = {{Formalizing Functions as Processes}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {5:1--5:21}, 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.5}, URN = {urn:nbn:de:0030-drops-183800}, doi = {10.4230/LIPIcs.ITP.2023.5}, annote = {Keywords: Lambda calculus, pi calculus, proof assistants, binders, Abella} }
David Kurniadi Angdinata and Junyan Xu. An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{angdinata_et_al:LIPIcs.ITP.2023.6, author = {Angdinata, David Kurniadi and Xu, Junyan}, title = {{An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {6:1--6: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.6}, URN = {urn:nbn:de:0030-drops-183817}, doi = {10.4230/LIPIcs.ITP.2023.6}, annote = {Keywords: formal math, algebraic geometry, elliptic curve, group law, Lean, mathlib} }
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman. A Proof-Producing Compiler for Blockchain Applications. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{avigad_et_al:LIPIcs.ITP.2023.7, author = {Avigad, Jeremy and Goldberg, Lior and Levit, David and Seginer, Yoav and Titelman, Alon}, title = {{A Proof-Producing Compiler for Blockchain Applications}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {7:1--7: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.7}, URN = {urn:nbn:de:0030-drops-183820}, doi = {10.4230/LIPIcs.ITP.2023.7}, annote = {Keywords: formal verification, smart contracts, interactive proof systems} }
Roger Bosman, Georgios Karachalias, and Tom Schrijvers. No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{bosman_et_al:LIPIcs.ITP.2023.8, author = {Bosman, Roger and Karachalias, Georgios and Schrijvers, Tom}, title = {{No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {8:1--8: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.8}, URN = {urn:nbn:de:0030-drops-183836}, doi = {10.4230/LIPIcs.ITP.2023.8}, annote = {Keywords: type inference, mechanization, let-polymorphism} }
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} }
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} }
Luís Cruz-Filipe and Fabrizio Montesi. Now It Compiles! Certified Automatic Repair of Uncompilable Protocols. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{cruzfilipe_et_al:LIPIcs.ITP.2023.11, author = {Cruz-Filipe, Lu{\'\i}s and Montesi, Fabrizio}, title = {{Now It Compiles! Certified Automatic Repair of Uncompilable Protocols}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {11:1--11: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.11}, URN = {urn:nbn:de:0030-drops-183867}, doi = {10.4230/LIPIcs.ITP.2023.11}, annote = {Keywords: choreographic programming, theorem proving, compilation, program repair} }
Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann. Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{dealmeidaborges_et_al:LIPIcs.ITP.2023.12, author = {de Almeida Borges, Ana and Casanueva Art{\'\i}s, Annal{\'\i} and Falleri, Jean-R\'{e}my and Gallego Arias, Emilio Jes\'{u}s and Martin-Dorel, \'{E}rik and Palmskog, Karl and Serebrenik, Alexander and Zimmermann, Th\'{e}o}, title = {{Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {12:1--12: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.12}, URN = {urn:nbn:de:0030-drops-183875}, doi = {10.4230/LIPIcs.ITP.2023.12}, annote = {Keywords: Coq, Community, Survey, Statistical Analysis} }
María Inés de Frutos-Fernández. Formalizing Norm Extensions and Applications to Number Theory. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{defrutosfernandez:LIPIcs.ITP.2023.13, author = {de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s}, title = {{Formalizing Norm Extensions and Applications to Number Theory}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {13:1--13: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.13}, URN = {urn:nbn:de:0030-drops-183880}, doi = {10.4230/LIPIcs.ITP.2023.13}, annote = {Keywords: formal mathematics, Lean, mathlib, algebraic number theory, p-adic analysis, Galois representations, p-adic Hodge theory} }
Lawrence Dunn, Val Tannen, and Steve Zdancewic. Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{dunn_et_al:LIPIcs.ITP.2023.14, author = {Dunn, Lawrence and Tannen, Val and Zdancewic, Steve}, title = {{Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {14:1--14:20}, 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.14}, URN = {urn:nbn:de:0030-drops-183891}, doi = {10.4230/LIPIcs.ITP.2023.14}, annote = {Keywords: Coq, category theory, formal metatheory, raw syntax, locally nameless} }
Martin Dvorak and Jasmin Blanchette. Closure Properties of General Grammars – Formally Verified. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{dvorak_et_al:LIPIcs.ITP.2023.15, author = {Dvorak, Martin and Blanchette, Jasmin}, title = {{Closure Properties of General Grammars – Formally Verified}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {15:1--15:16}, 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.15}, URN = {urn:nbn:de:0030-drops-183906}, doi = {10.4230/LIPIcs.ITP.2023.15}, annote = {Keywords: Lean, type-0 grammars, recursively enumerable languages, Kleene star} }
Jarl G. Taxerås Flaten. Formalising Yoneda Ext in Univalent Foundations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{flaten:LIPIcs.ITP.2023.16, author = {Flaten, Jarl G. Taxer\r{a}s}, title = {{Formalising Yoneda Ext in Univalent Foundations}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {16:1--16: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.16}, URN = {urn:nbn:de:0030-drops-183911}, doi = {10.4230/LIPIcs.ITP.2023.16}, annote = {Keywords: homotopy type theory, homological algebra, Yoneda Ext, formalisation, Coq} }
Simon Guilloud, Sankalp Gambhir, and Viktor Kunčak. LISA - A Modern Proof System. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{guilloud_et_al:LIPIcs.ITP.2023.17, author = {Guilloud, Simon and Gambhir, Sankalp and Kun\v{c}ak, Viktor}, title = {{LISA - A Modern Proof System}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {17:1--17: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.17}, URN = {urn:nbn:de:0030-drops-183922}, doi = {10.4230/LIPIcs.ITP.2023.17}, annote = {Keywords: Proof assistant, First Order Logic, Set Theory} }
Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{hirata_et_al:LIPIcs.ITP.2023.18, author = {Hirata, Michikazu and Minamide, Yasuhiko and Sato, Tetsuya}, title = {{Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {18:1--18: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.18}, URN = {urn:nbn:de:0030-drops-183933}, doi = {10.4230/LIPIcs.ITP.2023.18}, annote = {Keywords: Higher-order probabilistic program, s-finite kernel, Quasi-Borel spaces, Isabelle/HOL} }
Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban. MizAR 60 for Mizar 50. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{jakubuv_et_al:LIPIcs.ITP.2023.19, author = {Jakub\r{u}v, Jan and Chvalovsk\'{y}, Karel and Goertzel, Zarathustra and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Mirek and Piotrowski, Bartosz and Schulz, Stephan and Suda, Martin and Urban, Josef}, title = {{MizAR 60 for Mizar 50}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {19:1--19:22}, 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.19}, URN = {urn:nbn:de:0030-drops-183942}, doi = {10.4230/LIPIcs.ITP.2023.19}, annote = {Keywords: Mizar, ENIGMA, Automated Reasoning, Machine Learning} }
Philipp Joram and Niccolò Veltri. Constructive Final Semantics of Finite Bags. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{joram_et_al:LIPIcs.ITP.2023.20, author = {Joram, Philipp and Veltri, Niccol\`{o}}, title = {{Constructive Final Semantics of Finite Bags}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {20:1--20: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.20}, URN = {urn:nbn:de:0030-drops-183954}, doi = {10.4230/LIPIcs.ITP.2023.20}, annote = {Keywords: finite bags, final coalgebra, homotopy type theory, Cubical Agda} }
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} }
Amelia Livingston. Group Cohomology in the Lean Community Library. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{livingston:LIPIcs.ITP.2023.22, author = {Livingston, Amelia}, title = {{Group Cohomology in the Lean Community Library}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {22:1--22: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.22}, URN = {urn:nbn:de:0030-drops-183974}, doi = {10.4230/LIPIcs.ITP.2023.22}, annote = {Keywords: formal math, Lean, mathlib, group cohomology, homological algebra} }
Oliver Nash. A Formalisation of Gallagher’s Ergodic Theorem. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{nash:LIPIcs.ITP.2023.23, author = {Nash, Oliver}, title = {{A Formalisation of Gallagher’s Ergodic Theorem}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {23:1--23:16}, 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.23}, URN = {urn:nbn:de:0030-drops-183981}, doi = {10.4230/LIPIcs.ITP.2023.23}, annote = {Keywords: Lean proof assistant, measure theory, metric number theory, ergodicity, Gallagher’s theorem, Duffin-Schaeffer conjecture} }
Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An Extensible User Interface for Lean 4. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{nawrocki_et_al:LIPIcs.ITP.2023.24, author = {Nawrocki, Wojciech and Ayers, Edward W. and Ebner, Gabriel}, title = {{An Extensible User Interface for Lean 4}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {24:1--24:20}, 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.24}, URN = {urn:nbn:de:0030-drops-183991}, doi = {10.4230/LIPIcs.ITP.2023.24}, annote = {Keywords: user interfaces, human-computer interaction, Lean} }
Pierre Pomeret-Coquot, Hélène Fargier, and Érik Martin-Dorel. Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{pomeretcoquot_et_al:LIPIcs.ITP.2023.25, author = {Pomeret-Coquot, Pierre and Fargier, H\'{e}l\`{e}ne and Martin-Dorel, \'{E}rik}, title = {{Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {25:1--25: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.25}, URN = {urn:nbn:de:0030-drops-184001}, doi = {10.4230/LIPIcs.ITP.2023.25}, annote = {Keywords: Game of Incomplete Information, Belief Function Theory, Coq Proof Assistant, SSReflect Proof Language, MathComp Library} }
Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer. Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{reichel_et_al:LIPIcs.ITP.2023.26, author = {Reichel, Tom and Henderson, R. Wesley and Touchet, Andrew and Gardner, Andrew and Ringer, Talia}, title = {{Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {26:1--26:20}, 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.26}, URN = {urn:nbn:de:0030-drops-184013}, doi = {10.4230/LIPIcs.ITP.2023.26}, annote = {Keywords: proof repair, datasets, benchmarks, machine learning, formal proof} }
Chengsong Tan and Christian Urban. POSIX Lexing with Bitcoded Derivatives. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{tan_et_al:LIPIcs.ITP.2023.27, author = {Tan, Chengsong and Urban, Christian}, title = {{POSIX Lexing with Bitcoded Derivatives}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {27:1--27: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.27}, URN = {urn:nbn:de:0030-drops-184027}, doi = {10.4230/LIPIcs.ITP.2023.27}, annote = {Keywords: POSIX matching and lexing, derivatives of regular expressions, Isabelle/HOL} }
Dawit Tirore, Jesper Bengtson, and Marco Carbone. A Sound and Complete Projection for Global Types. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{tirore_et_al:LIPIcs.ITP.2023.28, author = {Tirore, Dawit and Bengtson, Jesper and Carbone, Marco}, title = {{A Sound and Complete Projection for Global Types}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {28:1--28: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.28}, URN = {urn:nbn:de:0030-drops-184039}, doi = {10.4230/LIPIcs.ITP.2023.28}, annote = {Keywords: Session types, Mechanisation, Projection, Coq} }
Balazs Toth and Tobias Nipkow. Real-Time Double-Ended Queue Verified (Proof Pearl). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{toth_et_al:LIPIcs.ITP.2023.29, author = {Toth, Balazs and Nipkow, Tobias}, title = {{Real-Time Double-Ended Queue Verified (Proof Pearl)}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {29:1--29: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.29}, URN = {urn:nbn:de:0030-drops-184044}, doi = {10.4230/LIPIcs.ITP.2023.29}, annote = {Keywords: Double-ended queue, data structures, verification, Isabelle} }
Niels van der Weide, Deivid Vale, and Cynthia Kop. Certifying Higher-Order Polynomial Interpretations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{vanderweide_et_al:LIPIcs.ITP.2023.30, author = {van der Weide, Niels and Vale, Deivid and Kop, Cynthia}, title = {{Certifying Higher-Order Polynomial Interpretations}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {30:1--30:20}, 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.30}, URN = {urn:nbn:de:0030-drops-184051}, doi = {10.4230/LIPIcs.ITP.2023.30}, annote = {Keywords: higher-order rewriting, Coq, termination, formalization} }
Niels F. W. Voorneveld. Slice Nondeterminism. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{voorneveld:LIPIcs.ITP.2023.31, author = {Voorneveld, Niels F. W.}, title = {{Slice Nondeterminism}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {31:1--31: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.31}, URN = {urn:nbn:de:0030-drops-184063}, doi = {10.4230/LIPIcs.ITP.2023.31}, annote = {Keywords: Category theory, Agda, Slice category, Nondeterministic functions, Powerset} }
Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, and Andrew W. Appel. Foundational Verification of Stateful P4 Packet Processing. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{wang_et_al:LIPIcs.ITP.2023.32, author = {Wang, Qinshi and Pan, Mengying and Wang, Shengyi and Doenges, Ryan and Beringer, Lennart and Appel, Andrew W.}, title = {{Foundational Verification of Stateful P4 Packet Processing}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {32:1--32:20}, 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.32}, URN = {urn:nbn:de:0030-drops-184077}, doi = {10.4230/LIPIcs.ITP.2023.32}, annote = {Keywords: Software Defined Networking, Verifiable P4, Stateful data plane programming} }
Yiming Xu and Michael Norrish. Dependently Sorted Theorem Proving for Mathematical Foundations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{xu_et_al:LIPIcs.ITP.2023.33, author = {Xu, Yiming and Norrish, Michael}, title = {{Dependently Sorted Theorem Proving for Mathematical Foundations}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {33:1--33: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.33}, URN = {urn:nbn:de:0030-drops-184085}, doi = {10.4230/LIPIcs.ITP.2023.33}, annote = {Keywords: first order logic, sorts, structural set theory, mechanised mathematics, foundation of mathematics, category theory} }
Akihisa Yamada and Jérémy Dubut. Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{yamada_et_al:LIPIcs.ITP.2023.34, author = {Yamada, Akihisa and Dubut, J\'{e}r\'{e}my}, title = {{Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {34:1--34:13}, 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.34}, URN = {urn:nbn:de:0030-drops-184092}, doi = {10.4230/LIPIcs.ITP.2023.34}, annote = {Keywords: Directed Sets, Completeness, Scott Continuous Functions, Ordinals, Isabelle/HOL} }
Jujian Zhang. Formalising the Proj Construction in Lean. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{zhang:LIPIcs.ITP.2023.35, author = {Zhang, Jujian}, title = {{Formalising the Proj Construction in Lean}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {35:1--35: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.35}, URN = {urn:nbn:de:0030-drops-184105}, doi = {10.4230/LIPIcs.ITP.2023.35}, annote = {Keywords: Lean, formalisation, algebraic geometry, scheme, Proj construction, projective geometry} }
Alex J. Best, Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi. Fermat’s Last Theorem for Regular Primes (Short Paper). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 36:1-36:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{best_et_al:LIPIcs.ITP.2023.36, author = {Best, Alex J. and Birkbeck, Christopher and Brasca, Riccardo and Rodriguez Boidi, Eric}, title = {{Fermat’s Last Theorem for Regular Primes}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {36:1--36:8}, 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.36}, URN = {urn:nbn:de:0030-drops-184115}, doi = {10.4230/LIPIcs.ITP.2023.36}, annote = {Keywords: Fermat’s Last Theorem, Cyclotomic fields, Interactive theorem proving, Lean} }
Adam Grabowski and Artur Korniłowicz. Implementing More Explicit Definitional Expansions in Mizar (Short Paper). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 37:1-37:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{grabowski_et_al:LIPIcs.ITP.2023.37, author = {Grabowski, Adam and Korni{\l}owicz, Artur}, title = {{Implementing More Explicit Definitional Expansions in Mizar}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {37:1--37:8}, 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.37}, URN = {urn:nbn:de:0030-drops-184121}, doi = {10.4230/LIPIcs.ITP.2023.37}, annote = {Keywords: Mizar, definitions, proof assistants, mechanization of proof} }
Christina Kohl and Aart Middeldorp. Formalizing Almost Development Closed Critical Pairs (Short Paper). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 38:1-38:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{kohl_et_al:LIPIcs.ITP.2023.38, author = {Kohl, Christina and Middeldorp, Aart}, title = {{Formalizing Almost Development Closed Critical Pairs}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {38:1--38:8}, 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.38}, URN = {urn:nbn:de:0030-drops-184130}, doi = {10.4230/LIPIcs.ITP.2023.38}, annote = {Keywords: Term rewriting, confluence, certification} }