Search dblp for Publications

export results for "toc:db/conf/itp/itp2021.bht:"

 download as .bib file

@inproceedings{DBLP:conf/itp/0001BL21,
  author       = {Andrei Popescu and
                  Thomas Bauereiss and
                  Peter Lammich},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Bounded-Deducibility Security (Invited Paper)},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {3:1--3:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.3},
  doi          = {10.4230/LIPICS.ITP.2021.3},
  timestamp    = {Mon, 21 Jun 2021 14:45:49 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/0001BL21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/0002DLT21,
  author       = {Matthias Brun and
                  S{\'{a}}ra Decova and
                  Andrea Lattuada and
                  Dmitriy Traytel},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Verified Progress Tracking for Timely Dataflow},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {10:1--10:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.10},
  doi          = {10.4230/LIPICS.ITP.2021.10},
  timestamp    = {Tue, 14 May 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/0002DLT21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/0002KSW21,
  author       = {Yannick Forster and
                  Fabian Kunze and
                  Gert Smolka and
                  Maxi Wuttke},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  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, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {19:1--19:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.19},
  doi          = {10.4230/LIPICS.ITP.2021.19},
  timestamp    = {Fri, 31 Mar 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/0002KSW21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/AyersJG21,
  author       = {Edward W. Ayers and
                  Mateja Jamnik and
                  William T. Gowers},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {A Graphical User Interface Framework for Formal Verification},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {4:1--4:16},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.4},
  doi          = {10.4230/LIPICS.ITP.2021.4},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/AyersJG21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BaanenDNC21,
  author       = {Anne Baanen and
                  Sander R. Dahmen and
                  Ashvni Narayanan and
                  Filippo A. E. Nuccio Mortarino Majno di Capriglio},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {A Formalization of Dedekind Domains and Class Groups of Global Fields},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {5:1--5:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.5},
  doi          = {10.4230/LIPICS.ITP.2021.5},
  timestamp    = {Sun, 02 Oct 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/BaanenDNC21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Baek21,
  author       = {Seulkee Baek},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {A Formally Verified Checker for First-Order Proofs},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {6:1--6:13},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.6},
  doi          = {10.4230/LIPICS.ITP.2021.6},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Baek21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BenzmullerF21,
  author       = {Christoph Benzm{\"{u}}ller and
                  David Fuenmayor},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Value-Oriented Legal Argumentation in Isabelle/HOL},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {7:1--7:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.7},
  doi          = {10.4230/LIPICS.ITP.2021.7},
  timestamp    = {Sat, 09 Apr 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/BenzmullerF21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BernardCMS21,
  author       = {Sophie Bernard and
                  Cyril Cohen and
                  Assia Mahboubi and
                  Pierre{-}Yves Strub},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Unsolvability of the Quintic Formalized in Dependent Type Theory},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {8:1--8:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.8},
  doi          = {10.4230/LIPICS.ITP.2021.8},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/BernardCMS21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Besson21,
  author       = {Fr{\'{e}}d{\'{e}}ric Besson},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Itauto: An Extensible Intuitionistic {SAT} Solver},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {9:1--9:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.9},
  doi          = {10.4230/LIPICS.ITP.2021.9},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Besson21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BylinskiKN21,
  author       = {Czeslaw Bylinski and
                  Artur Kornilowicz and
                  Adam Naumowicz},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Syntactic-Semantic Form of Mizar Articles},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {11:1--11:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.11},
  doi          = {10.4230/LIPICS.ITP.2021.11},
  timestamp    = {Sun, 25 Jul 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/BylinskiKN21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Chen21,
  author       = {Joshua Chen},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Homotopy Type Theory in Isabelle},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {12:1--12:8},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.12},
  doi          = {10.4230/LIPICS.ITP.2021.12},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Chen21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/CicconeDZ21,
  author       = {Luca Ciccone and
                  Francesco Dagnino and
                  Elena Zucca},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Flexible Coinduction in Agda},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {13:1--13:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.13},
  doi          = {10.4230/LIPICS.ITP.2021.13},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/CicconeDZ21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/CordwellTP21,
  author       = {Katherine Cordwell and
                  Yong Kiam Tan and
                  Andr{\'{e}} Platzer},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {A Verified Decision Procedure for Univariate Real Arithmetic with
                  the {BKR} Algorithm},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {14:1--14:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.14},
  doi          = {10.4230/LIPICS.ITP.2021.14},
  timestamp    = {Mon, 03 Jan 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/CordwellTP21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Cruz-FilipeMP21,
  author       = {Lu{\'{\i}}s Cruz{-}Filipe and
                  Fabrizio Montesi and
                  Marco Peressotti},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Formalising a Turing-Complete Choreographic Language in Coq},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {15:1--15:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.15},
  doi          = {10.4230/LIPICS.ITP.2021.15},
  timestamp    = {Thu, 14 Oct 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Cruz-FilipeMP21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Doczkal21,
  author       = {Christian Doczkal},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {A Variant of Wagner's Theorem Based on Combinatorial Hypermaps},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {17:1--17:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.17},
  doi          = {10.4230/LIPICS.ITP.2021.17},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Doczkal21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Doorn21,
  author       = {Floris van Doorn},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Formalized Haar Measure},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {18:1--18:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.18},
  doi          = {10.4230/LIPICS.ITP.2021.18},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Doorn21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/GaherK21,
  author       = {Lennard G{\"{a}}her and
                  Fabian Kunze},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Mechanising Complexity Theory: The Cook-Levin Theorem in Coq},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {20:1--20:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.20},
  doi          = {10.4230/LIPICS.ITP.2021.20},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/GaherK21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Hietala0HL021,
  author       = {Kesha Hietala and
                  Robert Rand and
                  Shih{-}Han Hung and
                  Liyi Li and
                  Michael Hicks},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Proving Quantum Programs Correct},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {21:1--21:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.21},
  doi          = {10.4230/LIPICS.ITP.2021.21},
  timestamp    = {Thu, 17 Aug 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Hietala0HL021.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/HolubS21,
  author       = {Stepan Holub and
                  Step{\'{a}}n Starosta},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Formalization of Basic Combinatorics on Words},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {22:1--22:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.22},
  doi          = {10.4230/LIPICS.ITP.2021.22},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/HolubS21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/KirstH21,
  author       = {Dominik Kirst and
                  Marc Hermes},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Synthetic Undecidability and Incompleteness of First-Order Axiom Systems
                  in Coq},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {23:1--23:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.23},
  doi          = {10.4230/LIPICS.ITP.2021.23},
  timestamp    = {Sat, 30 Sep 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/KirstH21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Lennon-Bertrand21,
  author       = {Meven Lennon{-}Bertrand},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Complete Bidirectional Typing for the Calculus of Inductive Constructions},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {24:1--24:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.24},
  doi          = {10.4230/LIPICS.ITP.2021.24},
  timestamp    = {Sun, 02 Oct 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Lennon-Bertrand21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Lochbihler21,
  author       = {Andreas Lochbihler},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {25:1--25:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.25},
  doi          = {10.4230/LIPICS.ITP.2021.25},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Lochbihler21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/LonKL21,
  author       = {Adrian De Lon and
                  Peter Koepke and
                  Anton Lorenzen},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {A Natural Formalization of the Mutilated Checkerboard Problem in Naproche},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {16:1--16:11},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.16},
  doi          = {10.4230/LIPICS.ITP.2021.16},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/LonKL21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/MaggesiB21,
  author       = {Marco Maggesi and
                  Cosimo {Perini Brogi}},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {A Formal Proof of Modal Completeness for Provability Logic},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {26:1--26:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.26},
  doi          = {10.4230/LIPICS.ITP.2021.26},
  timestamp    = {Mon, 26 Jun 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/MaggesiB21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/MunozAMDNAAR21,
  author       = {C{\'{e}}sar A. Mu{\~{n}}oz and
                  Mauricio Ayala{-}Rinc{\'{o}}n and
                  Mariano M. Moscato and
                  Aaron Dutle and
                  Anthony J. Narkawicz and
                  Ariane Alves Almeida and
                  Andr{\'{e}}ia B. Avelar and
                  Thiago Mendon{\c{c}}a Ferreira Ramos},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Formal Verification of Termination Criteria for First-Order Recursive
                  Functions},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {27:1--27:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.27},
  doi          = {10.4230/LIPICS.ITP.2021.27},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/MunozAMDNAAR21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Myreen21,
  author       = {Magnus O. Myreen},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {The CakeML Project's Quest for Ever Stronger Correctness Theorems
                  (Invited Paper)},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {1:1--1:10},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.1},
  doi          = {10.4230/LIPICS.ITP.2021.1},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Myreen21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/NatarajanSS21,
  author       = {Raja Natarajan and
                  Suneel Sarswat and
                  Abhishek Kr Singh},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Verified Double Sided Auctions for Financial Markets},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {28:1--28:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.28},
  doi          = {10.4230/LIPICS.ITP.2021.28},
  timestamp    = {Tue, 21 Mar 2023 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/NatarajanSS21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/NigronD21,
  author       = {Pierre Nigron and
                  Pierre{-}{\'{E}}variste Dagand},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Reaching for the Star: Tale of a Monad in Coq},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {29:1--29:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.29},
  doi          = {10.4230/LIPICS.ITP.2021.29},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/NigronD21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Polikarpova21,
  author       = {Nadia Polikarpova},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Synthesis of Safe Pointer-Manipulating Programs (Invited Talk)},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {2:1--2:1},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.2},
  doi          = {10.4230/LIPICS.ITP.2021.2},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Polikarpova21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Slind21,
  author       = {Konrad Slind},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Specifying Message Formats with Contiguity Types},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {30:1--30:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.30},
  doi          = {10.4230/LIPICS.ITP.2021.30},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Slind21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Thery21,
  author       = {Laurent Th{\'{e}}ry},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Proof Pearl : Playing with the Tower of Hanoi Formally},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {31:1--31:16},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.31},
  doi          = {10.4230/LIPICS.ITP.2021.31},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Thery21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/X21,
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Front Matter, Table of Contents, Preface, Conference Organization},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {0:1--0:8},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.0},
  doi          = {10.4230/LIPICS.ITP.2021.0},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/X21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/ZhangHK0LXBMPZ21,
  author       = {Hengchu Zhang and
                  Wolf Honor{\'{e}} and
                  Nicolas Koh and
                  Yao Li and
                  Yishuai Li and
                  Li{-}yao Xia and
                  Lennart Beringer and
                  William Mansky and
                  Benjamin C. Pierce and
                  Steve Zdancewic},
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {Verifying an {HTTP} Key-Value Server with Interaction Trees and {VST}},
  booktitle    = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  pages        = {32:1--32:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2021.32},
  doi          = {10.4230/LIPICS.ITP.2021.32},
  timestamp    = {Sat, 09 Apr 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/ZhangHK0LXBMPZ21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/itp/2021,
  editor       = {Liron Cohen and
                  Cezary Kaliszyk},
  title        = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series       = {LIPIcs},
  volume       = {193},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2021},
  url          = {https://www.dagstuhl.de/dagpub/978-3-95977-188-7},
  isbn         = {978-3-95977-188-7},
  timestamp    = {Mon, 21 Jun 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/2021.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
a service of  Schloss Dagstuhl - Leibniz Center for Informatics

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.