default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSearch 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 = {Wed, 21 Aug 2024 22:46:00 +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 = {Sun, 06 Oct 2024 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 = {Wed, 21 Aug 2024 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/2021.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
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.
retrieved on 2025-02-03 15:26 CET from data curated by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
