12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 1-560, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Magnus O. Myreen. The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper). In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 1:1-1:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Nadia Polikarpova. Synthesis of Safe Pointer-Manipulating Programs (Invited Talk). In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Andrei Popescu, Thomas Bauereiss, and Peter Lammich. Bounded-Deducibility Security (Invited Paper). In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Edward W. Ayers, Mateja Jamnik, and W. T. Gowers. A Graphical User Interface Framework for Formal Verification. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio. A Formalization of Dedekind Domains and Class Groups of Global Fields. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Seulkee Baek. A Formally Verified Checker for First-Order Proofs. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 6:1-6:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Christoph Benzmüller and David Fuenmayor. Value-Oriented Legal Argumentation in Isabelle/HOL. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Frédéric Besson. Itauto: An Extensible Intuitionistic SAT Solver. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Matthias Brun, Sára Decova, Andrea Lattuada, and Dmitriy Traytel. Verified Progress Tracking for Timely Dataflow. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Czesław Byliński, Artur Korniłowicz, and Adam Naumowicz. Syntactic-Semantic Form of Mizar Articles. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Joshua Chen. Homotopy Type Theory in Isabelle. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 12:1-12:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Luca Ciccone, Francesco Dagnino, and Elena Zucca. Flexible Coinduction in Agda. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Katherine Cordwell, Yong Kiam Tan, and André Platzer. A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Formalising a Turing-Complete Choreographic Language in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Adrian De Lon, Peter Koepke, and Anton Lorenzen. A Natural Formalization of the Mutilated Checkerboard Problem in Naproche. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 16:1-16:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Christian Doczkal. A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Floris van Doorn. Formalized Haar Measure. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Yannick Forster, Fabian Kunze, Gert Smolka, and Maximilian Wuttke. A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Lennard Gäher and Fabian Kunze. Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks. Proving Quantum Programs Correct. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Štěpán Holub and Štěpán Starosta. Formalization of Basic Combinatorics on Words. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Dominik Kirst and Marc Hermes. Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Meven Lennon-Bertrand. Complete Bidirectional Typing for the Calculus of Inductive Constructions. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Andreas Lochbihler. A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Marco Maggesi and Cosimo Perini Brogi. A Formal Proof of Modal Completeness for Provability Logic. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Cesar A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron M. Dutle, Anthony J. Narkawicz, Ariane A. Almeida, Andréia B. Avelar, and Thiago M. Ferreira Ramos. Formal Verification of Termination Criteria for First-Order Recursive Functions. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Raja Natarajan, Suneel Sarswat, and Abhishek Kr Singh. Verified Double Sided Auctions for Financial Markets. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Pierre Nigron and Pierre-Évariste Dagand. Reaching for the Star: Tale of a Monad in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 29:1-29:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Konrad Slind. Specifying Message Formats with Contiguity Types. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Laurent Théry. Proof Pearl : Playing with the Tower of Hanoi Formally. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic. Verifying an HTTP Key-Value Server with Interaction Trees and VST. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@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} }
Feedback for Dagstuhl Publishing