@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}
}