@Proceedings{andronick_et_al:LIPIcs.ITP.2022,
title = {{LIPIcs, Volume 237, ITP 2022, Complete Volume}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {1--602},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022},
URN = {urn:nbn:de:0030-drops-167080},
doi = {10.4230/LIPIcs.ITP.2022},
annote = {Keywords: LIPIcs, Volume 237, ITP 2022, Complete Volume}
}
@InProceedings{andronick_et_al:LIPIcs.ITP.2022.0,
author = {Andronick, June and de Moura, Leonardo},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {0:i--0:x},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.0},
URN = {urn:nbn:de:0030-drops-167097},
doi = {10.4230/LIPIcs.ITP.2022.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
@InProceedings{felty:LIPIcs.ITP.2022.1,
author = {Felty, Amy},
title = {{Modelling and Verifying Properties of Biological Neural Networks}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.1},
URN = {urn:nbn:de:0030-drops-167100},
doi = {10.4230/LIPIcs.ITP.2022.1},
annote = {Keywords: Neuronal networks, Model checking, Theorem proving, Coq}
}
@InProceedings{zhan:LIPIcs.ITP.2022.2,
author = {Zhan, Bohua},
title = {{User Interface Design in the HolPy Theorem Prover}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.2},
URN = {urn:nbn:de:0030-drops-167117},
doi = {10.4230/LIPIcs.ITP.2022.2},
annote = {Keywords: Proof assistants, User interface, Proof automation}
}
@InProceedings{abrahamsson_et_al:LIPIcs.ITP.2022.3,
author = {Abrahamsson, Oskar and Myreen, Magnus O. and Kumar, Ramana and Sewell, Thomas},
title = {{Candle: A Verified Implementation of HOL Light}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {3:1--3:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.3},
URN = {urn:nbn:de:0030-drops-167126},
doi = {10.4230/LIPIcs.ITP.2022.3},
annote = {Keywords: Prover soundness, Higher-order logic, Interactive theorem proving}
}
@InProceedings{baanen:LIPIcs.ITP.2022.4,
author = {Baanen, Anne},
title = {{Use and Abuse of Instance Parameters in the Lean Mathematical Library}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {4:1--4:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.4},
URN = {urn:nbn:de:0030-drops-167131},
doi = {10.4230/LIPIcs.ITP.2022.4},
annote = {Keywords: formalization of mathematics, dependent type theory, typeclasses, algebraic hierarchy, Lean prover}
}
@InProceedings{bapanapally_et_al:LIPIcs.ITP.2022.5,
author = {Bapanapally, Jagadish and Gamboa, Ruben},
title = {{A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {5:1--5:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.5},
URN = {urn:nbn:de:0030-drops-167142},
doi = {10.4230/LIPIcs.ITP.2022.5},
annote = {Keywords: ACL2(r), Banach-Tarski, Rotations}
}
@InProceedings{becker_et_al:LIPIcs.ITP.2022.6,
author = {Becker, Heiko and Tekriwal, Mohit and Darulova, Eva and Volkova, Anastasia and Jeannin, Jean-Baptiste},
title = {{Dandelion: Certified Approximations of Elementary Functions}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {6:1--6:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.6},
URN = {urn:nbn:de:0030-drops-167155},
doi = {10.4230/LIPIcs.ITP.2022.6},
annote = {Keywords: elementary functions, approximation, certificate checking}
}
@InProceedings{biernacka_et_al:LIPIcs.ITP.2022.7,
author = {Biernacka, Ma{\l}gorzata and Charatonik, Witold and Drab, Tomasz},
title = {{The Zoo of Lambda-Calculus Reduction Strategies, And Coq}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {7:1--7:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.7},
URN = {urn:nbn:de:0030-drops-167165},
doi = {10.4230/LIPIcs.ITP.2022.7},
annote = {Keywords: Lambda calculus, Reduction strategies, Coq}
}
@InProceedings{desharnais_et_al:LIPIcs.ITP.2022.8,
author = {Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius},
title = {{Seventeen Provers Under the Hammer}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.8},
URN = {urn:nbn:de:0030-drops-167178},
doi = {10.4230/LIPIcs.ITP.2022.8},
annote = {Keywords: Automatic theorem proving, interactive theorem proving, proof assistants}
}
@InProceedings{dillies_et_al:LIPIcs.ITP.2022.9,
author = {Dillies, Ya\"{e}l and Mehta, Bhavik},
title = {{Formalising Szemer\'{e}di’s Regularity Lemma in Lean}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {9:1--9:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.9},
URN = {urn:nbn:de:0030-drops-167185},
doi = {10.4230/LIPIcs.ITP.2022.9},
annote = {Keywords: Lean, formalisation, formal proof, graph theory, combinatorics, additive combinatorics, Szemer\'{e}di’s Regularity Lemma, Roth’s Theorem}
}
@InProceedings{dupuis_et_al:LIPIcs.ITP.2022.10,
author = {Dupuis, Fr\'{e}d\'{e}ric and Lewis, Robert Y. and Macbeth, Heather},
title = {{Formalized functional analysis with semilinear maps}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {10:1--10:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.10},
URN = {urn:nbn:de:0030-drops-167191},
doi = {10.4230/LIPIcs.ITP.2022.10},
annote = {Keywords: Functional analysis, Lean, linear algebra, semilinear, Hilbert space}
}
@InProceedings{edmonds_et_al:LIPIcs.ITP.2022.11,
author = {Edmonds, Chelsea and Paulson, Lawrence C.},
title = {{Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.11},
URN = {urn:nbn:de:0030-drops-167204},
doi = {10.4230/LIPIcs.ITP.2022.11},
annote = {Keywords: Isabelle/HOL, Mathematical Formalisation, Fisher’s Inequality, Linear Algebra, Formal Proof Techniques, Combinatorics}
}
@InProceedings{forster_et_al:LIPIcs.ITP.2022.12,
author = {Forster, Yannick and Kunze, Fabian and Lauermann, Nils},
title = {{Synthetic Kolmogorov Complexity in Coq}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {12:1--12:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.12},
URN = {urn:nbn:de:0030-drops-167219},
doi = {10.4230/LIPIcs.ITP.2022.12},
annote = {Keywords: Kolmogorov complexity, computability theory, random numbers, constructive matemathics, synthetic computability theory, constructive type theory, Coq}
}
@InProceedings{from_et_al:LIPIcs.ITP.2022.13,
author = {From, Asta Halkj{\ae}r and Jacobsen, Frederik Krogsdal},
title = {{Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {13:1--13:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.13},
URN = {urn:nbn:de:0030-drops-167221},
doi = {10.4230/LIPIcs.ITP.2022.13},
annote = {Keywords: Isabelle/HOL, SeCaV, First-Order Logic, Prover, Soundness, Completeness}
}
@InProceedings{defrutosfernandez:LIPIcs.ITP.2022.14,
author = {de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s},
title = {{Formalizing the Ring of Ad\`{e}les of a Global Field}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.14},
URN = {urn:nbn:de:0030-drops-167232},
doi = {10.4230/LIPIcs.ITP.2022.14},
annote = {Keywords: formal math, algebraic number theory, class field theory, Lean, mathlib}
}
@InProceedings{gengelbach_et_al:LIPIcs.ITP.2022.15,
author = {Gengelbach, Arve and \r{A}man Pohjola, Johannes},
title = {{A Verified Cyclicity Checker: For Theories with Overloaded Constants}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {15:1--15:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.15},
URN = {urn:nbn:de:0030-drops-167240},
doi = {10.4230/LIPIcs.ITP.2022.15},
annote = {Keywords: cyclicity, non-termination, ad-hoc overloading, definitions, Isabelle/HOL}
}
@InProceedings{goertzel_et_al:LIPIcs.ITP.2022.16,
author = {Goertzel, Zarathustra A. and Jakub\r{u}v, Jan and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Miroslav and Piepenbrock, Jelle and Urban, Josef},
title = {{The Isabelle ENIGMA}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {16:1--16:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.16},
URN = {urn:nbn:de:0030-drops-167253},
doi = {10.4230/LIPIcs.ITP.2022.16},
annote = {Keywords: E Prover, ENIGMA, Premise Selection, Isabelle/Sledgehammer}
}
@InProceedings{gross_et_al:LIPIcs.ITP.2022.17,
author = {Gross, Jason and Erbsen, Andres and Philipoom, Jade and Poddar-Agrawal, Miraya and Chlipala, Adam},
title = {{Accelerating Verified-Compiler Development with a Verified Rewriting Engine}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {17:1--17:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.17},
URN = {urn:nbn:de:0030-drops-167262},
doi = {10.4230/LIPIcs.ITP.2022.17},
annote = {Keywords: compiler verification, rewriting engines, cryptography}
}
@InProceedings{gross_et_al:LIPIcs.ITP.2022.18,
author = {Gross, Jason and Zimmermann, Th\'{e}o and Poddar-Agrawal, Miraya and Chlipala, Adam},
title = {{Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {18:1--18:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.18},
URN = {urn:nbn:de:0030-drops-167273},
doi = {10.4230/LIPIcs.ITP.2022.18},
annote = {Keywords: debugging, automatic test-case reduction, Coq, bug minimizer}
}
@InProceedings{hostert_et_al:LIPIcs.ITP.2022.19,
author = {Hostert, Johannes and Dudenhefner, Andrej and Kirst, Dominik},
title = {{Undecidability of Dyadic First-Order Logic in Coq}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {19:1--19:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.19},
URN = {urn:nbn:de:0030-drops-167280},
doi = {10.4230/LIPIcs.ITP.2022.19},
annote = {Keywords: undecidability, synthetic computability, first-order logic, Coq}
}
@InProceedings{kanabar_et_al:LIPIcs.ITP.2022.20,
author = {Kanabar, Hrutvik and Fox, Anthony C. J. and Myreen, Magnus O.},
title = {{Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {20:1--20:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.20},
URN = {urn:nbn:de:0030-drops-167295},
doi = {10.4230/LIPIcs.ITP.2022.20},
annote = {Keywords: Compiler verification, ISA specification, HOL4, interactive theorem proving}
}
@InProceedings{karayel:LIPIcs.ITP.2022.21,
author = {Karayel, Emin},
title = {{Formalization of Randomized Approximation Algorithms for Frequency Moments}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {21:1--21:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.21},
URN = {urn:nbn:de:0030-drops-167308},
doi = {10.4230/LIPIcs.ITP.2022.21},
annote = {Keywords: Formal Verification, Isabelle/HOL, Randomized Algorithms, Frequency Moments}
}
@InProceedings{kirst:LIPIcs.ITP.2022.22,
author = {Kirst, Dominik},
title = {{Computational Back-And-Forth Arguments in Constructive Type Theory}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {22:1--22:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.22},
URN = {urn:nbn:de:0030-drops-167311},
doi = {10.4230/LIPIcs.ITP.2022.22},
annote = {Keywords: back-and-forth method, computable isomorphisms, Coq}
}
@InProceedings{kudryashov:LIPIcs.ITP.2022.23,
author = {Kudryashov, Yury},
title = {{Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {23:1--23:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.23},
URN = {urn:nbn:de:0030-drops-167326},
doi = {10.4230/LIPIcs.ITP.2022.23},
annote = {Keywords: divergence theorem, Green’s theorem, Gauge integral, Cauchy integral formula, Cauchy-Goursat theorem, complex analysis}
}
@InProceedings{lammich:LIPIcs.ITP.2022.24,
author = {Lammich, Peter},
title = {{Refinement of Parallel Algorithms down to LLVM}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {24:1--24:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.24},
URN = {urn:nbn:de:0030-drops-167333},
doi = {10.4230/LIPIcs.ITP.2022.24},
annote = {Keywords: Isabelle, Concurrent Separation Logic, Parallel Sorting, LLVM}
}
@InProceedings{magaud:LIPIcs.ITP.2022.25,
author = {Magaud, Nicolas},
title = {{Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {25:1--25:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.25},
URN = {urn:nbn:de:0030-drops-167349},
doi = {10.4230/LIPIcs.ITP.2022.25},
annote = {Keywords: Coq, projective geometry, finite models, spreads, packings, PG(3, 2)}
}
@InProceedings{pak_et_al:LIPIcs.ITP.2022.26,
author = {P\k{a}k, Karol and Kaliszyk, Cezary},
title = {{Formalizing a Diophantine Representation of the Set of Prime Numbers}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {26:1--26:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.26},
URN = {urn:nbn:de:0030-drops-167350},
doi = {10.4230/LIPIcs.ITP.2022.26},
annote = {Keywords: DPRM theorem, Polynomial reduction, prime numbers}
}
@InProceedings{pohjola_et_al:LIPIcs.ITP.2022.27,
author = {Pohjola, Johannes \r{A}man and G\'{o}mez-Londo\~{n}o, Alejandro and Shaker, James and Norrish, Michael},
title = {{Kalas: A Verified, End-To-End Compiler for a Choreographic Language}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {27:1--27:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.27},
URN = {urn:nbn:de:0030-drops-167368},
doi = {10.4230/LIPIcs.ITP.2022.27},
annote = {Keywords: Choreographies, Interactive Theorem Proving, Compiler Verification}
}
@InProceedings{prinz_et_al:LIPIcs.ITP.2022.28,
author = {Prinz, Jacob and Kavvos, G. A. and Lampropoulos, Leonidas},
title = {{Deeper Shallow Embeddings}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {28:1--28:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.28},
URN = {urn:nbn:de:0030-drops-167379},
doi = {10.4230/LIPIcs.ITP.2022.28},
annote = {Keywords: type theory, shallow embedding, deep embedding, Agda}
}
@InProceedings{sakaguchi:LIPIcs.ITP.2022.29,
author = {Sakaguchi, Kazuhiko},
title = {{Reflexive Tactics for Algebra, Revisited}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {29:1--29:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.29},
URN = {urn:nbn:de:0030-drops-167385},
doi = {10.4230/LIPIcs.ITP.2022.29},
annote = {Keywords: Coq, Elpi, \lambdaProlog, Mathematical Components, algebraic structures, packed classes, canonical structures, proof by reflection}
}
@InProceedings{stoughton_et_al:LIPIcs.ITP.2022.30,
author = {Stoughton, Alley and Chen, Carol and Gaboardi, Marco and Qu, Weihao},
title = {{Formalizing Algorithmic Bounds in the Query Model in EasyCrypt}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {30:1--30:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.30},
URN = {urn:nbn:de:0030-drops-167399},
doi = {10.4230/LIPIcs.ITP.2022.30},
annote = {Keywords: query model, lower bound, upper bound, adversary argument, EasyCrypt}
}
@InProceedings{vajjha_et_al:LIPIcs.ITP.2022.31,
author = {Vajjha, Koundinya and Trager, Barry and Shinnar, Avraham and Pestun, Vasily},
title = {{Formalization of a Stochastic Approximation Theorem}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {31:1--31:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.31},
URN = {urn:nbn:de:0030-drops-167402},
doi = {10.4230/LIPIcs.ITP.2022.31},
annote = {Keywords: Formal Verification, Stochastic Approximation, Stochastic Processes, Probability Theory, Optimization Algorithms}
}
@InProceedings{yeager_et_al:LIPIcs.ITP.2022.32,
author = {Yeager, Jared and Moss, J. Eliot B. and Norrish, Michael and Thomas, Philip S.},
title = {{Mechanizing Soundness of Off-Policy Evaluation}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {32:1--32:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.32},
URN = {urn:nbn:de:0030-drops-167413},
doi = {10.4230/LIPIcs.ITP.2022.32},
annote = {Keywords: Formal Methods, HOL4, Reinforcement Learning, Off-Policy Evaluation, Concentration Inequality, Hoeffding}
}
@InProceedings{zhan_et_al:LIPIcs.ITP.2022.33,
author = {Zhan, Bohua and Lv, Yi and Wang, Shuling and Zhao, Gehang and Hao, Jifeng and Ye, Hong and Xia, Bican},
title = {{Compositional Verification of Interacting Systems Using Event Monads}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {33:1--33:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.33},
URN = {urn:nbn:de:0030-drops-167420},
doi = {10.4230/LIPIcs.ITP.2022.33},
annote = {Keywords: Hoare Logic, Compositional Verification, Events}
}
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