@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing