LIPIcs, Volume 193
ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)
Editors: Liron Cohen and Cezary Kaliszyk
Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)
Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun. Inductive Continuity via Brouwer Trees. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 37:1-37:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{cohen_et_al:LIPIcs.MFCS.2023.37, author = {Cohen, Liron and da Rocha Paiva, Bruno and Rahli, Vincent and Tosun, Ayberk}, title = {{Inductive Continuity via Brouwer Trees}}, booktitle = {48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)}, pages = {37:1--37:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-292-1}, ISSN = {1868-8969}, year = {2023}, volume = {272}, editor = {Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.37}, URN = {urn:nbn:de:0030-drops-185718}, doi = {10.4230/LIPIcs.MFCS.2023.37}, annote = {Keywords: Continuity, Dialogue trees, Stateful computations, Intuitionistic Logic, Extensional Type Theory, Constructive Type Theory, Realizability, Theorem proving, Agda} }
Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
Liron Cohen and Vincent Rahli. Realizing Continuity Using Stateful Computations. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 15:1-15:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
@InProceedings{cohen_et_al:LIPIcs.CSL.2023.15, author = {Cohen, Liron and Rahli, Vincent}, title = {{Realizing Continuity Using Stateful Computations}}, booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)}, pages = {15:1--15:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-264-8}, ISSN = {1868-8969}, year = {2023}, volume = {252}, editor = {Klin, Bartek and Pimentel, Elaine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.15}, URN = {urn:nbn:de:0030-drops-174761}, doi = {10.4230/LIPIcs.CSL.2023.15}, annote = {Keywords: Continuity, Stateful computations, Intuitionism, Extensional Type Theory, Constructive Type Theory, Realizability, Theorem proving, Agda} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Liron Cohen and Vincent Rahli. Constructing Unprejudiced Extensional Type Theories with Choices via Modalities. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 10:1-10:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{cohen_et_al:LIPIcs.FSCD.2022.10, author = {Cohen, Liron and Rahli, Vincent}, title = {{Constructing Unprejudiced Extensional Type Theories with Choices via Modalities}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {10:1--10:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-233-4}, ISSN = {1868-8969}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.10}, URN = {urn:nbn:de:0030-drops-162917}, doi = {10.4230/LIPIcs.FSCD.2022.10}, annote = {Keywords: Intuitionism, Extensional Type Theory, Constructive Type Theory, Realizability, Choice sequences, References, Classical Logic, Theorem proving, Agda} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Liron Cohen and Cezary Kaliszyk. LIPIcs, Volume 193, ITP 2021, Complete Volume. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 1-560, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@Proceedings{cohen_et_al:LIPIcs.ITP.2021, title = {{LIPIcs, Volume 193, ITP 2021, Complete Volume}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {1--560}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021}, URN = {urn:nbn:de:0030-drops-138943}, doi = {10.4230/LIPIcs.ITP.2021}, annote = {Keywords: LIPIcs, Volume 193, ITP 2021, Complete Volume} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Liron Cohen and Cezary Kaliszyk. Front Matter, Table of Contents, Preface, Conference Organization. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 0:i-0:viii, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{cohen_et_al:LIPIcs.ITP.2021.0, author = {Cohen, Liron and Kaliszyk, Cezary}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {0:i--0:viii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.0}, URN = {urn:nbn:de:0030-drops-138955}, doi = {10.4230/LIPIcs.ITP.2021.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Magnus O. Myreen. The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper). In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 1:1-1:10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{myreen:LIPIcs.ITP.2021.1, author = {Myreen, Magnus O.}, title = {{The CakeML Project’s Quest for Ever Stronger Correctness Theorems}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {1:1--1:10}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.1}, URN = {urn:nbn:de:0030-drops-138963}, doi = {10.4230/LIPIcs.ITP.2021.1}, annote = {Keywords: Program verification, interactive theorem proving} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Nadia Polikarpova. Synthesis of Safe Pointer-Manipulating Programs (Invited Talk). In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, p. 2:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{polikarpova:LIPIcs.ITP.2021.2, author = {Polikarpova, Nadia}, title = {{Synthesis of Safe Pointer-Manipulating Programs}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.2}, URN = {urn:nbn:de:0030-drops-138975}, doi = {10.4230/LIPIcs.ITP.2021.2}, annote = {Keywords: Program Synthesis, Separation Logic, Proof Search} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Andrei Popescu, Thomas Bauereiss, and Peter Lammich. Bounded-Deducibility Security (Invited Paper). In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 3:1-3:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{popescu_et_al:LIPIcs.ITP.2021.3, author = {Popescu, Andrei and Bauereiss, Thomas and Lammich, Peter}, title = {{Bounded-Deducibility Security}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {3:1--3:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.3}, URN = {urn:nbn:de:0030-drops-138982}, doi = {10.4230/LIPIcs.ITP.2021.3}, annote = {Keywords: Information-flow security, Unwinding proof method, Compositionality, Verification} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Edward W. Ayers, Mateja Jamnik, and W. T. Gowers. A Graphical User Interface Framework for Formal Verification. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 4:1-4:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{ayers_et_al:LIPIcs.ITP.2021.4, author = {Ayers, Edward W. and Jamnik, Mateja and Gowers, W. T.}, title = {{A Graphical User Interface Framework for Formal Verification}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {4:1--4:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.4}, URN = {urn:nbn:de:0030-drops-138996}, doi = {10.4230/LIPIcs.ITP.2021.4}, annote = {Keywords: User Interfaces, ITP} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio. A Formalization of Dedekind Domains and Class Groups of Global Fields. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 5:1-5:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{baanen_et_al:LIPIcs.ITP.2021.5, author = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni and Nuccio Mortarino Majno di Capriglio, Filippo A. E.}, title = {{A Formalization of Dedekind Domains and Class Groups of Global Fields}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {5:1--5:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.5}, URN = {urn:nbn:de:0030-drops-139004}, doi = {10.4230/LIPIcs.ITP.2021.5}, annote = {Keywords: formal math, algebraic number theory, commutative algebra, Lean, mathlib} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Seulkee Baek. A Formally Verified Checker for First-Order Proofs. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 6:1-6:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{baek:LIPIcs.ITP.2021.6, author = {Baek, Seulkee}, title = {{A Formally Verified Checker for First-Order Proofs}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {6:1--6:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.6}, URN = {urn:nbn:de:0030-drops-139010}, doi = {10.4230/LIPIcs.ITP.2021.6}, annote = {Keywords: TESC, TPTP, TSTP, ATP} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Christoph Benzmüller and David Fuenmayor. Value-Oriented Legal Argumentation in Isabelle/HOL. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 7:1-7:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{benzmuller_et_al:LIPIcs.ITP.2021.7, author = {Benzm\"{u}ller, Christoph and Fuenmayor, David}, title = {{Value-Oriented Legal Argumentation in Isabelle/HOL}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {7:1--7:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.7}, URN = {urn:nbn:de:0030-drops-139028}, doi = {10.4230/LIPIcs.ITP.2021.7}, annote = {Keywords: Higher order logic, preference logic, shallow embedding, legal reasoning} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 8:1-8:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{bernard_et_al:LIPIcs.ITP.2021.8, author = {Bernard, Sophie and Cohen, Cyril and Mahboubi, Assia and Strub, Pierre-Yves}, title = {{Unsolvability of the Quintic Formalized in Dependent Type Theory}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.8}, URN = {urn:nbn:de:0030-drops-139038}, doi = {10.4230/LIPIcs.ITP.2021.8}, annote = {Keywords: Galois theory, Coq, Mathematical Components, Dependent Type Theory, Abel-Ruffini, General quintic} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Frédéric Besson. Itauto: An Extensible Intuitionistic SAT Solver. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 9:1-9:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{besson:LIPIcs.ITP.2021.9, author = {Besson, Fr\'{e}d\'{e}ric}, title = {{Itauto: An Extensible Intuitionistic SAT Solver}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {9:1--9:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.9}, URN = {urn:nbn:de:0030-drops-139043}, doi = {10.4230/LIPIcs.ITP.2021.9}, annote = {Keywords: SAT solver, proof by reflection} }
Feedback for Dagstuhl Publishing