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