@Proceedings{cohen_et_al:LIPIcs.ITP.2021,
  title =	{{LIPIcs, Volume 193, ITP 2021, Complete Volume}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{1--560},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021},
  URN =		{urn:nbn:de:0030-drops-138943},
  doi =		{10.4230/LIPIcs.ITP.2021},
  annote =	{Keywords: LIPIcs, Volume 193, ITP 2021, Complete Volume}
}
@InProceedings{cohen_et_al:LIPIcs.ITP.2021.0,
  author =	{Cohen, Liron and Kaliszyk, Cezary},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{0:i--0:viii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.0},
  URN =		{urn:nbn:de:0030-drops-138955},
  doi =		{10.4230/LIPIcs.ITP.2021.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
@InProceedings{myreen:LIPIcs.ITP.2021.1,
  author =	{Myreen, Magnus O.},
  title =	{{The CakeML Project’s Quest for Ever Stronger Correctness Theorems}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{1:1--1:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.1},
  URN =		{urn:nbn:de:0030-drops-138963},
  doi =		{10.4230/LIPIcs.ITP.2021.1},
  annote =	{Keywords: Program verification, interactive theorem proving}
}
@InProceedings{polikarpova:LIPIcs.ITP.2021.2,
  author =	{Polikarpova, Nadia},
  title =	{{Synthesis of Safe Pointer-Manipulating Programs}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.2},
  URN =		{urn:nbn:de:0030-drops-138975},
  doi =		{10.4230/LIPIcs.ITP.2021.2},
  annote =	{Keywords: Program Synthesis, Separation Logic, Proof Search}
}
@InProceedings{popescu_et_al:LIPIcs.ITP.2021.3,
  author =	{Popescu, Andrei and Bauereiss, Thomas and Lammich, Peter},
  title =	{{Bounded-Deducibility Security}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{3:1--3:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.3},
  URN =		{urn:nbn:de:0030-drops-138982},
  doi =		{10.4230/LIPIcs.ITP.2021.3},
  annote =	{Keywords: Information-flow security, Unwinding proof method, Compositionality, Verification}
}
@InProceedings{ayers_et_al:LIPIcs.ITP.2021.4,
  author =	{Ayers, Edward W. and Jamnik, Mateja and Gowers, W. T.},
  title =	{{A Graphical User Interface Framework for Formal Verification}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{4:1--4:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.4},
  URN =		{urn:nbn:de:0030-drops-138996},
  doi =		{10.4230/LIPIcs.ITP.2021.4},
  annote =	{Keywords: User Interfaces, ITP}
}
@InProceedings{baanen_et_al:LIPIcs.ITP.2021.5,
  author =	{Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni and Nuccio Mortarino Majno di Capriglio, Filippo A. E.},
  title =	{{A Formalization of Dedekind Domains and Class Groups of Global Fields}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.5},
  URN =		{urn:nbn:de:0030-drops-139004},
  doi =		{10.4230/LIPIcs.ITP.2021.5},
  annote =	{Keywords: formal math, algebraic number theory, commutative algebra, Lean, mathlib}
}
@InProceedings{baek:LIPIcs.ITP.2021.6,
  author =	{Baek, Seulkee},
  title =	{{A Formally Verified Checker for First-Order Proofs}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{6:1--6:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.6},
  URN =		{urn:nbn:de:0030-drops-139010},
  doi =		{10.4230/LIPIcs.ITP.2021.6},
  annote =	{Keywords: TESC, TPTP, TSTP, ATP}
}
@InProceedings{benzmuller_et_al:LIPIcs.ITP.2021.7,
  author =	{Benzm\"{u}ller, Christoph and Fuenmayor, David},
  title =	{{Value-Oriented Legal Argumentation in Isabelle/HOL}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.7},
  URN =		{urn:nbn:de:0030-drops-139028},
  doi =		{10.4230/LIPIcs.ITP.2021.7},
  annote =	{Keywords: Higher order logic, preference logic, shallow embedding, legal reasoning}
}
@InProceedings{bernard_et_al:LIPIcs.ITP.2021.8,
  author =	{Bernard, Sophie and Cohen, Cyril and Mahboubi, Assia and Strub, Pierre-Yves},
  title =	{{Unsolvability of the Quintic Formalized in Dependent Type Theory}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.8},
  URN =		{urn:nbn:de:0030-drops-139038},
  doi =		{10.4230/LIPIcs.ITP.2021.8},
  annote =	{Keywords: Galois theory, Coq, Mathematical Components, Dependent Type Theory, Abel-Ruffini, General quintic}
}
@InProceedings{besson:LIPIcs.ITP.2021.9,
  author =	{Besson, Fr\'{e}d\'{e}ric},
  title =	{{Itauto: An Extensible Intuitionistic SAT Solver}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.9},
  URN =		{urn:nbn:de:0030-drops-139043},
  doi =		{10.4230/LIPIcs.ITP.2021.9},
  annote =	{Keywords: SAT solver, proof by reflection}
}
@InProceedings{brun_et_al:LIPIcs.ITP.2021.10,
  author =	{Brun, Matthias and Decova, S\'{a}ra and Lattuada, Andrea and Traytel, Dmitriy},
  title =	{{Verified Progress Tracking for Timely Dataflow}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{10:1--10:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.10},
  URN =		{urn:nbn:de:0030-drops-139057},
  doi =		{10.4230/LIPIcs.ITP.2021.10},
  annote =	{Keywords: safety, distributed systems, timely dataflow, Isabelle/HOL}
}
@InProceedings{bylinski_et_al:LIPIcs.ITP.2021.11,
  author =	{Byli\'{n}ski, Czes{\l}aw and Korni{\l}owicz, Artur and Naumowicz, Adam},
  title =	{{Syntactic-Semantic Form of Mizar Articles}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{11:1--11:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.11},
  URN =		{urn:nbn:de:0030-drops-139064},
  doi =		{10.4230/LIPIcs.ITP.2021.11},
  annote =	{Keywords: Mizar system, mathematical knowledge representation, XML representation}
}
@InProceedings{chen:LIPIcs.ITP.2021.12,
  author =	{Chen, Joshua},
  title =	{{Homotopy Type Theory in Isabelle}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{12:1--12:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.12},
  URN =		{urn:nbn:de:0030-drops-139072},
  doi =		{10.4230/LIPIcs.ITP.2021.12},
  annote =	{Keywords: Proof assistants, Logical frameworks, Dependent type theory, Homotopy type theory}
}
@InProceedings{ciccone_et_al:LIPIcs.ITP.2021.13,
  author =	{Ciccone, Luca and Dagnino, Francesco and Zucca, Elena},
  title =	{{Flexible Coinduction in Agda}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{13:1--13:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.13},
  URN =		{urn:nbn:de:0030-drops-139083},
  doi =		{10.4230/LIPIcs.ITP.2021.13},
  annote =	{Keywords: inference systems, induction, coinduction}
}
@InProceedings{cordwell_et_al:LIPIcs.ITP.2021.14,
  author =	{Cordwell, Katherine and Tan, Yong Kiam and Platzer, Andr\'{e}},
  title =	{{A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.14},
  URN =		{urn:nbn:de:0030-drops-139099},
  doi =		{10.4230/LIPIcs.ITP.2021.14},
  annote =	{Keywords: quantifier elimination, matrix, theorem proving, real arithmetic}
}
@InProceedings{cruzfilipe_et_al:LIPIcs.ITP.2021.15,
  author =	{Cruz-Filipe, Lu{\'\i}s and Montesi, Fabrizio and Peressotti, Marco},
  title =	{{Formalising a Turing-Complete Choreographic Language in Coq}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.15},
  URN =		{urn:nbn:de:0030-drops-139109},
  doi =		{10.4230/LIPIcs.ITP.2021.15},
  annote =	{Keywords: Choreographic Programming, Formalisation, Turing Completeness}
}
@InProceedings{delon_et_al:LIPIcs.ITP.2021.16,
  author =	{De Lon, Adrian and Koepke, Peter and Lorenzen, Anton},
  title =	{{A Natural Formalization of the Mutilated Checkerboard Problem in Naproche}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{16:1--16:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.16},
  URN =		{urn:nbn:de:0030-drops-139112},
  doi =		{10.4230/LIPIcs.ITP.2021.16},
  annote =	{Keywords: checkerboard, formalization, formal mathematics, controlled language}
}
@InProceedings{doczkal:LIPIcs.ITP.2021.17,
  author =	{Doczkal, Christian},
  title =	{{A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{17:1--17:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.17},
  URN =		{urn:nbn:de:0030-drops-139123},
  doi =		{10.4230/LIPIcs.ITP.2021.17},
  annote =	{Keywords: Coq, MathComp, Graph-Theory, Hypermaps, Planarity}
}
@InProceedings{vandoorn:LIPIcs.ITP.2021.18,
  author =	{van Doorn, Floris},
  title =	{{Formalized Haar Measure}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.18},
  URN =		{urn:nbn:de:0030-drops-139139},
  doi =		{10.4230/LIPIcs.ITP.2021.18},
  annote =	{Keywords: Haar measure, measure theory, Bochner integral, Lean, interactive theorem proving, formalized mathematics}
}
@InProceedings{forster_et_al:LIPIcs.ITP.2021.19,
  author =	{Forster, Yannick and Kunze, Fabian and Smolka, Gert and Wuttke, Maximilian},
  title =	{{A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value \lambda-Calculus}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{19:1--19:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.19},
  URN =		{urn:nbn:de:0030-drops-139142},
  doi =		{10.4230/LIPIcs.ITP.2021.19},
  annote =	{Keywords: formalizations of computational models, computability theory, Coq, time complexity, Turing machines, lambda calculus, Hoare logic}
}
@InProceedings{gaher_et_al:LIPIcs.ITP.2021.20,
  author =	{G\"{a}her, Lennard and Kunze, Fabian},
  title =	{{Mechanising Complexity Theory: The Cook-Levin Theorem in Coq}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.20},
  URN =		{urn:nbn:de:0030-drops-139154},
  doi =		{10.4230/LIPIcs.ITP.2021.20},
  annote =	{Keywords: computational model, NP completeness, Coq, Cook, Levin}
}
@InProceedings{hietala_et_al:LIPIcs.ITP.2021.21,
  author =	{Hietala, Kesha and Rand, Robert and Hung, Shih-Han and Li, Liyi and Hicks, Michael},
  title =	{{Proving Quantum Programs Correct}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{21:1--21:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.21},
  URN =		{urn:nbn:de:0030-drops-139160},
  doi =		{10.4230/LIPIcs.ITP.2021.21},
  annote =	{Keywords: Formal Verification, Quantum Computing, Proof Engineering}
}
@InProceedings{holub_et_al:LIPIcs.ITP.2021.22,
  author =	{Holub, \v{S}t\v{e}p\'{a}n and Starosta, \v{S}t\v{e}p\'{a}n},
  title =	{{Formalization of Basic Combinatorics on Words}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.22},
  URN =		{urn:nbn:de:0030-drops-139177},
  doi =		{10.4230/LIPIcs.ITP.2021.22},
  annote =	{Keywords: combinatorics on words, formalization, Isabelle/HOL}
}
@InProceedings{kirst_et_al:LIPIcs.ITP.2021.23,
  author =	{Kirst, Dominik and Hermes, Marc},
  title =	{{Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{23:1--23:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.23},
  URN =		{urn:nbn:de:0030-drops-139188},
  doi =		{10.4230/LIPIcs.ITP.2021.23},
  annote =	{Keywords: undecidability, synthetic computability, first-order logic, incompleteness, Peano arithmetic, ZF set theory, constructive type theory, Coq}
}
@InProceedings{lennonbertrand:LIPIcs.ITP.2021.24,
  author =	{Lennon-Bertrand, Meven},
  title =	{{Complete Bidirectional Typing for the Calculus of Inductive Constructions}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.24},
  URN =		{urn:nbn:de:0030-drops-139194},
  doi =		{10.4230/LIPIcs.ITP.2021.24},
  annote =	{Keywords: Bidirectional Typing, Calculus of Inductive Constructions, Coq, Proof Assistants}
}
@InProceedings{lochbihler:LIPIcs.ITP.2021.25,
  author =	{Lochbihler, Andreas},
  title =	{{A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.25},
  URN =		{urn:nbn:de:0030-drops-139204},
  doi =		{10.4230/LIPIcs.ITP.2021.25},
  annote =	{Keywords: flow network, optimization, infinite graph, Isabelle/HOL}
}
@InProceedings{maggesi_et_al:LIPIcs.ITP.2021.26,
  author =	{Maggesi, Marco and Perini Brogi, Cosimo},
  title =	{{A Formal Proof of Modal Completeness for Provability Logic}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.26},
  URN =		{urn:nbn:de:0030-drops-139215},
  doi =		{10.4230/LIPIcs.ITP.2021.26},
  annote =	{Keywords: Provability Logic, Higher-Order Logic, Mechanized Mathematics, HOL Light Theorem Prover}
}
@InProceedings{munoz_et_al:LIPIcs.ITP.2021.27,
  author =	{Mu\~{n}oz, Cesar A. and Ayala-Rinc\'{o}n, Mauricio and Moscato, Mariano M. and Dutle, Aaron M. and Narkawicz, Anthony J. and Almeida, Ariane A. and Avelar, Andr\'{e}ia B. and M. Ferreira Ramos, Thiago},
  title =	{{Formal Verification of Termination Criteria for First-Order Recursive Functions}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.27},
  URN =		{urn:nbn:de:0030-drops-139228},
  doi =		{10.4230/LIPIcs.ITP.2021.27},
  annote =	{Keywords: Formal Verification, Termination, Calling Context Graph, PVS}
}
@InProceedings{natarajan_et_al:LIPIcs.ITP.2021.28,
  author =	{Natarajan, Raja and Sarswat, Suneel and Singh, Abhishek Kr},
  title =	{{Verified Double Sided Auctions for Financial Markets}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.28},
  URN =		{urn:nbn:de:0030-drops-139230},
  doi =		{10.4230/LIPIcs.ITP.2021.28},
  annote =	{Keywords: Double Sided Auction, Formal Verification, Financial Markets, Proof Assistant}
}
@InProceedings{nigron_et_al:LIPIcs.ITP.2021.29,
  author =	{Nigron, Pierre and Dagand, Pierre-\'{E}variste},
  title =	{{Reaching for the Star: Tale of a Monad in Coq}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{29:1--29:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.29},
  URN =		{urn:nbn:de:0030-drops-139241},
  doi =		{10.4230/LIPIcs.ITP.2021.29},
  annote =	{Keywords: monads, hoare logic, separation logic, Coq}
}
@InProceedings{slind:LIPIcs.ITP.2021.30,
  author =	{Slind, Konrad},
  title =	{{Specifying Message Formats with Contiguity Types}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{30:1--30:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.30},
  URN =		{urn:nbn:de:0030-drops-139252},
  doi =		{10.4230/LIPIcs.ITP.2021.30},
  annote =	{Keywords: Logic, verification, formal language theory, message format languages}
}
@InProceedings{thery:LIPIcs.ITP.2021.31,
  author =	{Th\'{e}ry, Laurent},
  title =	{{Proof Pearl : Playing with the Tower of Hanoi Formally}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{31:1--31:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.31},
  URN =		{urn:nbn:de:0030-drops-139267},
  doi =		{10.4230/LIPIcs.ITP.2021.31},
  annote =	{Keywords: Mathematical logic, Formal proof, Hanoi Tower}
}
@InProceedings{zhang_et_al:LIPIcs.ITP.2021.32,
  author =	{Zhang, Hengchu and Honor\'{e}, Wolf and Koh, Nicolas and Li, Yao and Li, Yishuai and Xia, Li-Yao and Beringer, Lennart and Mansky, William and Pierce, Benjamin and Zdancewic, Steve},
  title =	{{Verifying an HTTP Key-Value Server with Interaction Trees and VST}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{32:1--32:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.32},
  URN =		{urn:nbn:de:0030-drops-139273},
  doi =		{10.4230/LIPIcs.ITP.2021.32},
  annote =	{Keywords: formal verification, Coq, HTTP, deep specification}
}