@Proceedings{bertot_et_al:LIPIcs.ITP.2024,
title = {{LIPIcs, Volume 309, ITP 2024, Complete Volume}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {1--714},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024},
URN = {urn:nbn:de:0030-drops-207277},
doi = {10.4230/LIPIcs.ITP.2024},
annote = {Keywords: LIPIcs, Volume 309, ITP 2024, Complete Volume}
}
@InProceedings{bertot_et_al:LIPIcs.ITP.2024.0,
author = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {0:i--0:xii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.0},
URN = {urn:nbn:de:0030-drops-207287},
doi = {10.4230/LIPIcs.ITP.2024.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
@InProceedings{nipkow:LIPIcs.ITP.2024.1,
author = {Nipkow, Tobias},
title = {{Alpha-Beta Pruning Verified}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {1:1--1:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.1},
URN = {urn:nbn:de:0030-drops-207294},
doi = {10.4230/LIPIcs.ITP.2024.1},
annote = {Keywords: Verification, Algorithmic Game Theory, Isabelle}
}
@InProceedings{blanqui:LIPIcs.ITP.2024.2,
author = {Blanqui, Fr\'{e}d\'{e}ric},
title = {{Translating Libraries of Definitions and Theorems Between Proof Systems}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.2},
URN = {urn:nbn:de:0030-drops-207307},
doi = {10.4230/LIPIcs.ITP.2024.2},
annote = {Keywords: Logical frameworks, proof systems interoperability, type theory}
}
@InProceedings{abdulaziz_et_al:LIPIcs.ITP.2024.3,
author = {Abdulaziz, Mohammad and Ammer, Thomas},
title = {{A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {3:1--3:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.3},
URN = {urn:nbn:de:0030-drops-207316},
doi = {10.4230/LIPIcs.ITP.2024.3},
annote = {Keywords: Network Flows, Formal Verification, Combinatorial Optimisation}
}
@InProceedings{affeldt_et_al:LIPIcs.ITP.2024.4,
author = {Affeldt, Reynald and Bruni, Alessandro and Komendantskaya, Ekaterina and \'{S}lusarz, Natalia and Stark, Kathrin},
title = {{Taming Differentiable Logics with Coq Formalisation}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {4:1--4:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.4},
URN = {urn:nbn:de:0030-drops-207325},
doi = {10.4230/LIPIcs.ITP.2024.4},
annote = {Keywords: Machine Learning, Loss Functions, Differentiable Logics, Logic and Semantics, Interactive Theorem Proving}
}
@InProceedings{affeldt_et_al:LIPIcs.ITP.2024.5,
author = {Affeldt, Reynald and Stone, Zachary},
title = {{A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {5:1--5:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.5},
URN = {urn:nbn:de:0030-drops-207330},
doi = {10.4230/LIPIcs.ITP.2024.5},
annote = {Keywords: Coq proof assistant, Mathematical Components library, Lebesgue integral, fundamental theorem of calculus}
}
@InProceedings{asgeirsson:LIPIcs.ITP.2024.6,
author = {Asgeirsson, Dagur},
title = {{Towards Solid Abelian Groups: A Formal Proof of N\"{o}beling’s Theorem}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {6:1--6:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.6},
URN = {urn:nbn:de:0030-drops-207347},
doi = {10.4230/LIPIcs.ITP.2024.6},
annote = {Keywords: Condensed mathematics, N\"{o}beling’s theorem, Lean, Mathlib, Interactive theorem proving}
}
@InProceedings{ballenghien_et_al:LIPIcs.ITP.2024.7,
author = {Ballenghien, Beno\^{i}t and Wolff, Burkhart},
title = {{An Operational Semantics in Isabelle/HOL-CSP}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {7:1--7:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.7},
URN = {urn:nbn:de:0030-drops-207355},
doi = {10.4230/LIPIcs.ITP.2024.7},
annote = {Keywords: Process-Algebra, Semantics, Concurrency, Computational Models, Theorem Proving, Isabelle/HOL}
}
@InProceedings{basold_et_al:LIPIcs.ITP.2024.8,
author = {Basold, Henning and Bruin, Peter and Lawson, Dominique},
title = {{The Directed Van Kampen Theorem in Lean}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.8},
URN = {urn:nbn:de:0030-drops-207368},
doi = {10.4230/LIPIcs.ITP.2024.8},
annote = {Keywords: Lean, Directed Topology, Van Kampen Theorem, Directed Homotopy Theory, Formalised Mathematics}
}
@InProceedings{bhat_et_al:LIPIcs.ITP.2024.9,
author = {Bhat, Siddharth and Keizer, Alex and Hughes, Chris and Goens, Andr\'{e}s and Grosser, Tobias},
title = {{Verifying Peephole Rewriting in SSA Compiler IRs}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {9:1--9:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.9},
URN = {urn:nbn:de:0030-drops-207372},
doi = {10.4230/LIPIcs.ITP.2024.9},
annote = {Keywords: compilers, semantics, mechanization, MLIR, SSA, regions, peephole rewrites}
}
@InProceedings{clune_et_al:LIPIcs.ITP.2024.10,
author = {Clune, Joshua and Qian, Yicheng and Bentkamp, Alexander and Avigad, Jeremy},
title = {{Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {10:1--10:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.10},
URN = {urn:nbn:de:0030-drops-207381},
doi = {10.4230/LIPIcs.ITP.2024.10},
annote = {Keywords: proof search, automatic theorem proving, interactive theorem proving, Lean, dependent type theory}
}
@InProceedings{delima_et_al:LIPIcs.ITP.2024.11,
author = {de Lima, Thaynara Arielly and Galdino, Andr\'{e} Luiz and de Oliveira Ribeiro, Bruno Berto and Ayala-Rinc\'{o}n, Mauricio},
title = {{A Formalization of the General Theory of Quaternions}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {11:1--11:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.11},
URN = {urn:nbn:de:0030-drops-207398},
doi = {10.4230/LIPIcs.ITP.2024.11},
annote = {Keywords: Theory of quaternions, Hamilton’s quaternions, Algebraic formalizations, PVS}
}
@InProceedings{desharnais_et_al:LIPIcs.ITP.2024.12,
author = {Desharnais, Martin and Toth, Balazs and Waldmann, Uwe and Blanchette, Jasmin and Tourret, Sophie},
title = {{A Modular Formalization of Superposition in Isabelle/HOL}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {12:1--12:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.12},
URN = {urn:nbn:de:0030-drops-207401},
doi = {10.4230/LIPIcs.ITP.2024.12},
annote = {Keywords: Superposition, verification, first-order logic, higher-order logic}
}
@InProceedings{ekici_et_al:LIPIcs.ITP.2024.13,
author = {Ekici, Burak and Yoshida, Nobuko},
title = {{Completeness of Asynchronous Session Tree Subtyping in Coq}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {13:1--13:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.13},
URN = {urn:nbn:de:0030-drops-207418},
doi = {10.4230/LIPIcs.ITP.2024.13},
annote = {Keywords: asynchronous multiparty session types, session trees, subtyping, Coq}
}
@InProceedings{faissole_et_al:LIPIcs.ITP.2024.14,
author = {Faissole, Florian and Geneau de Lamarli\`{e}re, Paul and Melquiond, Guillaume},
title = {{End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.14},
URN = {urn:nbn:de:0030-drops-207420},
doi = {10.4230/LIPIcs.ITP.2024.14},
annote = {Keywords: Program verification, floating-point arithmetic, formal proof, automated reasoning, mathematical library}
}
@InProceedings{garrigue_et_al:LIPIcs.ITP.2024.15,
author = {Garrigue, Jacques and Saikawa, Takafumi},
title = {{Typed Compositional Quantum Computation with Lenses}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {15:1--15:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.15},
URN = {urn:nbn:de:0030-drops-207431},
doi = {10.4230/LIPIcs.ITP.2024.15},
annote = {Keywords: quantum programming, semantics, lens, currying, Coq, MathComp}
}
@InProceedings{gauthier_et_al:LIPIcs.ITP.2024.16,
author = {Gauthier, Thibault and Brown, Chad E.},
title = {{A Formal Proof of R(4,5)=25}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {16:1--16:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.16},
URN = {urn:nbn:de:0030-drops-207446},
doi = {10.4230/LIPIcs.ITP.2024.16},
annote = {Keywords: Ramsey numbers, SAT solvers, symmetry breaking, generalization, HOL4}
}
@InProceedings{gruetter_et_al:LIPIcs.ITP.2024.17,
author = {Gruetter, Samuel and Bourgeat, Thomas and Chlipala, Adam},
title = {{Verifying Software Emulation of an Unsupported Hardware Instruction}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {17:1--17:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.17},
URN = {urn:nbn:de:0030-drops-207452},
doi = {10.4230/LIPIcs.ITP.2024.17},
annote = {Keywords: Software verification, Software-hardware boundary, Coq}
}
@InProceedings{guilloud_et_al:LIPIcs.ITP.2024.18,
author = {Guilloud, Simon and Gambhir, Sankalp and Gilot, Andrea and Kun\v{c}ak, Viktor},
title = {{Mechanized HOL Reasoning in Set Theory}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {18:1--18:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.18},
URN = {urn:nbn:de:0030-drops-207464},
doi = {10.4230/LIPIcs.ITP.2024.18},
annote = {Keywords: Proof assistant, First Order Logic, Set Theory, Higher Order Logic}
}
@InProceedings{hermes_et_al:LIPIcs.ITP.2024.19,
author = {Hermes, Marc and Krebbers, Robbert},
title = {{Modular Verification of Intrusive List and Tree Data Structures in Separation Logic}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {19:1--19:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.19},
URN = {urn:nbn:de:0030-drops-207478},
doi = {10.4230/LIPIcs.ITP.2024.19},
annote = {Keywords: Separation Logic, Program Verification, Data Structures, Iris, Coq}
}
@InProceedings{hilhorst_et_al:LIPIcs.ITP.2024.20,
author = {Hilhorst, Dennis and North, Paige Randall},
title = {{Formalizing the Algebraic Small Object Argument in UniMath}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {20:1--20:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.20},
URN = {urn:nbn:de:0030-drops-207486},
doi = {10.4230/LIPIcs.ITP.2024.20},
annote = {Keywords: formalization of mathematics, univalent foundations, model category theory, algebraic small object argument, coq, unimath}
}
@InProceedings{hirata:LIPIcs.ITP.2024.21,
author = {Hirata, Michikazu},
title = {{A Formalization of the L\'{e}vy-Prokhorov Metric in Isabelle/HOL}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {21:1--21:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.21},
URN = {urn:nbn:de:0030-drops-207492},
doi = {10.4230/LIPIcs.ITP.2024.21},
annote = {Keywords: formalization of mathematics, measure theory, metric spaces, topology, L\'{e}vy-Prokhorov metric, Prokhorov’s theorem, Isabelle/HOL}
}
@InProceedings{huch_et_al:LIPIcs.ITP.2024.22,
author = {Huch, Fabian and Wenzel, Makarius},
title = {{Distributed Parallel Build for the Isabelle Archive of Formal Proofs}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {22:1--22:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.22},
URN = {urn:nbn:de:0030-drops-207505},
doi = {10.4230/LIPIcs.ITP.2024.22},
annote = {Keywords: Interactive theorem proving, Isabelle, Archive of Formal Proofs, Theorem prover technology, Distributed computing, Schedule optimization}
}
@InProceedings{jackson_et_al:LIPIcs.ITP.2024.23,
author = {Jackson, Vincent and Murray, Toby and Rizkallah, Christine},
title = {{A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {23:1--23:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.23},
URN = {urn:nbn:de:0030-drops-207510},
doi = {10.4230/LIPIcs.ITP.2024.23},
annote = {Keywords: verification, concurrency, rely-guarantee, separation logic, resource algebras}
}
@InProceedings{kim:LIPIcs.ITP.2024.24,
author = {Kim, Dohan},
title = {{An Isabelle/HOL Formalization of Narrowing and Multiset Narrowing for E-Unifiability, Reachability and Infeasibility}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {24:1--24:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.24},
URN = {urn:nbn:de:0030-drops-207525},
doi = {10.4230/LIPIcs.ITP.2024.24},
annote = {Keywords: Narrowing, Multiset Narrowing, Unifiability, Reachability}
}
@InProceedings{kwan_et_al:LIPIcs.ITP.2024.25,
author = {Kwan, Carl and Hunt Jr., Warren A.},
title = {{Formalizing the Cholesky Factorization Theorem}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {25:1--25:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.25},
URN = {urn:nbn:de:0030-drops-207532},
doi = {10.4230/LIPIcs.ITP.2024.25},
annote = {Keywords: Numerical linear algebra, Cholesky factorization theorem, Matrix decomposition, Automated reasoning, ACL2}
}
@InProceedings{leray_et_al:LIPIcs.ITP.2024.26,
author = {Leray, Yann and Gilbert, Ga\"{e}tan and Tabareau, Nicolas and Winterhalter, Th\'{e}o},
title = {{The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {26:1--26:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.26},
URN = {urn:nbn:de:0030-drops-207545},
doi = {10.4230/LIPIcs.ITP.2024.26},
annote = {Keywords: type theory, dependent types, rewrite rules, type preservation, Coq}
}
@InProceedings{massot:LIPIcs.ITP.2024.27,
author = {Massot, Patrick},
title = {{Teaching Mathematics Using Lean and Controlled Natural Language}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {27:1--27:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.27},
URN = {urn:nbn:de:0030-drops-207550},
doi = {10.4230/LIPIcs.ITP.2024.27},
annote = {Keywords: mathematics teaching, proof assistant, controlled natural language}
}
@InProceedings{obendrauf_et_al:LIPIcs.ITP.2024.28,
author = {Obendrauf, Kai and Baanen, Anne and Koopmann, Patrick and Stebletsova, Vera},
title = {{Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {28:1--28:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.28},
URN = {urn:nbn:de:0030-drops-207560},
doi = {10.4230/LIPIcs.ITP.2024.28},
annote = {Keywords: Multi-agent systems, Coalition Logic, Epistemic Logic, common knowledge, completeness, formal methods, Lean prover}
}
@InProceedings{pak_et_al:LIPIcs.ITP.2024.29,
author = {P\k{a}k, Karol and Kaliszyk, Cezary},
title = {{Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {29:1--29:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.29},
URN = {urn:nbn:de:0030-drops-207573},
doi = {10.4230/LIPIcs.ITP.2024.29},
annote = {Keywords: Surreal numbers, Conway normal form, Mizar}
}
@InProceedings{park_et_al:LIPIcs.ITP.2024.30,
author = {Park, Sewon and Thies, Holger},
title = {{A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {30:1--30:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.30},
URN = {urn:nbn:de:0030-drops-207581},
doi = {10.4230/LIPIcs.ITP.2024.30},
annote = {Keywords: Exact real computation, Taylor models, Analytic functions, Computable analysis, Program extraction}
}
@InProceedings{rau_et_al:LIPIcs.ITP.2024.31,
author = {Rau, Martin and Nipkow, Tobias},
title = {{A Verified Earley Parser}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {31:1--31:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.31},
URN = {urn:nbn:de:0030-drops-207596},
doi = {10.4230/LIPIcs.ITP.2024.31},
annote = {Keywords: Verification, Parsers, Earley, Isabelle}
}
@InProceedings{saffrich:LIPIcs.ITP.2024.32,
author = {Saffrich, Hannes},
title = {{Abstractions for Multi-Sorted Substitutions}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {32:1--32:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.32},
URN = {urn:nbn:de:0030-drops-207609},
doi = {10.4230/LIPIcs.ITP.2024.32},
annote = {Keywords: Agda, Metatheory, Framework}
}
@InProceedings{seo_et_al:LIPIcs.ITP.2024.33,
author = {Seo, Audrey and Lam, Christopher and Grossman, Dan and Ringer, Talia},
title = {{Correctly Compiling Proofs About Programs Without Proving Compilers Correct}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {33:1--33:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.33},
URN = {urn:nbn:de:0030-drops-207612},
doi = {10.4230/LIPIcs.ITP.2024.33},
annote = {Keywords: proof transformations, compiler validation, program logics, proof engineering}
}
@InProceedings{soldevila_et_al:LIPIcs.ITP.2024.34,
author = {Soldevila, Mallku and Ribeiro, Rodrigo and Ziliani, Beta},
title = {{Redex2Coq: Towards a Theory of Decidability of Redex’s Reduction Semantics}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {34:1--34:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.34},
URN = {urn:nbn:de:0030-drops-207629},
doi = {10.4230/LIPIcs.ITP.2024.34},
annote = {Keywords: Coq, PLT Redex, Reduction semantics}
}
@InProceedings{subercaseaux_et_al:LIPIcs.ITP.2024.35,
author = {Subercaseaux, Bernardo and Nawrocki, Wojciech and Gallicchio, James and Codel, Cayden and Carneiro, Mario and Heule, Marijn J. H.},
title = {{Formal Verification of the Empty Hexagon Number}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {35:1--35:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.35},
URN = {urn:nbn:de:0030-drops-207633},
doi = {10.4230/LIPIcs.ITP.2024.35},
annote = {Keywords: Empty Hexagon Number, Discrete Computational Geometry, Erd\H{o}s-Szekeres}
}
@InProceedings{tolmach_et_al:LIPIcs.ITP.2024.36,
author = {Tolmach, Andrew and Chhak, Chris and Anderson, Sean},
title = {{Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {36:1--36:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.36},
URN = {urn:nbn:de:0030-drops-207643},
doi = {10.4230/LIPIcs.ITP.2024.36},
annote = {Keywords: Compiler verification, C language semantics, Coq proof assistant}
}
@InProceedings{vandoorn_et_al:LIPIcs.ITP.2024.37,
author = {van Doorn, Floris and Macbeth, Heather},
title = {{Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {37:1--37:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.37},
URN = {urn:nbn:de:0030-drops-207657},
doi = {10.4230/LIPIcs.ITP.2024.37},
annote = {Keywords: Sobolev inequality, measure theory, Lean, formalized mathematics}
}
@InProceedings{zeuner_et_al:LIPIcs.ITP.2024.38,
author = {Zeuner, Max and Hutzler, Matthias},
title = {{The Functor of Points Approach to Schemes in Cubical Agda}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {38:1--38:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.38},
URN = {urn:nbn:de:0030-drops-207667},
doi = {10.4230/LIPIcs.ITP.2024.38},
annote = {Keywords: Schemes, Algebraic Geometry, Category Theory, Cubical Agda, Homotopy Type Theory and Univalent Foundations, Constructive Mathematics}
}
@InProceedings{affeldt_et_al:LIPIcs.ITP.2024.39,
author = {Affeldt, Reynald and Barrett, Clark and Bruni, Alessandro and Daukantas, Ieva and Khan, Harun and Saikawa, Takafumi and Sch\"{u}rmann, Carsten},
title = {{Robust Mean Estimation by All Means}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {39:1--39:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.39},
URN = {urn:nbn:de:0030-drops-207679},
doi = {10.4230/LIPIcs.ITP.2024.39},
annote = {Keywords: robust statistics, probability theory, formal verification}
}
@InProceedings{eberl_et_al:LIPIcs.ITP.2024.40,
author = {Eberl, Manuel and Bordg, Anthony and Paulson, Lawrence C. and Li, Wenda},
title = {{Formalising Half of a Graduate Textbook on Number Theory}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {40:1--40:7},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.40},
URN = {urn:nbn:de:0030-drops-207686},
doi = {10.4230/LIPIcs.ITP.2024.40},
annote = {Keywords: Isabelle/HOL, number theory, complex analysis, formalisation of mathematics}
}
@InProceedings{ezeh:LIPIcs.ITP.2024.41,
author = {Ezeh, Sam},
title = {{Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4}},
booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
pages = {41:1--41:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-337-9},
ISSN = {1868-8969},
year = {2024},
volume = {309},
editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.41},
URN = {urn:nbn:de:0030-drops-207690},
doi = {10.4230/LIPIcs.ITP.2024.41},
annote = {Keywords: Interactive theorem proving, Lean4, Graphical User Interface}
}
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