default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID12th ITP 2021: Rome, Italy (Virtual Conference)
- Liron Cohen
, Cezary Kaliszyk:
12th International Conference on Interactive Theorem Proving, ITP 2021, Rome, Italy (Virtual Conference), June 29 - July 1, 2021. LIPIcs 193, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2021, ISBN 978-3-95977-188-7 - Front Matter, Table of Contents, Preface, Conference Organization. 0:1-0:8
- Magnus O. Myreen:
The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper). 1:1-1:10 - Nadia Polikarpova:
Synthesis of Safe Pointer-Manipulating Programs (Invited Talk). 2:1-2:1 - Andrei Popescu, Thomas Bauereiss, Peter Lammich:
Bounded-Deducibility Security (Invited Paper). 3:1-3:20 - Edward W. Ayers, Mateja Jamnik, William T. Gowers:
A Graphical User Interface Framework for Formal Verification. 4:1-4:16 - Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio Mortarino Majno di Capriglio:
A Formalization of Dedekind Domains and Class Groups of Global Fields. 5:1-5:19 - Seulkee Baek:
A Formally Verified Checker for First-Order Proofs. 6:1-6:13 - Christoph Benzmüller, David Fuenmayor:
Value-Oriented Legal Argumentation in Isabelle/HOL. 7:1-7:20 - Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub:
Unsolvability of the Quintic Formalized in Dependent Type Theory. 8:1-8:18 - Frédéric Besson:
Itauto: An Extensible Intuitionistic SAT Solver. 9:1-9:18 - Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel:
Verified Progress Tracking for Timely Dataflow. 10:1-10:20 - Czeslaw Bylinski, Artur Kornilowicz, Adam Naumowicz:
Syntactic-Semantic Form of Mizar Articles. 11:1-11:17 - Joshua Chen:
Homotopy Type Theory in Isabelle. 12:1-12:8 - Luca Ciccone, Francesco Dagnino, Elena Zucca:
Flexible Coinduction in Agda. 13:1-13:19 - Katherine Cordwell, Yong Kiam Tan, André Platzer:
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. 14:1-14:20 - Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti:
Formalising a Turing-Complete Choreographic Language in Coq. 15:1-15:18 - Adrian De Lon, Peter Koepke, Anton Lorenzen:
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche. 16:1-16:11 - Christian Doczkal:
A Variant of Wagner's Theorem Based on Combinatorial Hypermaps. 17:1-17:17 - Floris van Doorn:
Formalized Haar Measure. 18:1-18:17 - Yannick Forster, Fabian Kunze, Gert Smolka, Maxi Wuttke:
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. 19:1-19:20 - Lennard Gäher, Fabian Kunze:
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. 20:1-20:18 - Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks:
Proving Quantum Programs Correct. 21:1-21:19 - Stepan Holub, Stepán Starosta:
Formalization of Basic Combinatorics on Words. 22:1-22:17 - Dominik Kirst, Marc Hermes:
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. 23:1-23:20 - Meven Lennon-Bertrand:
Complete Bidirectional Typing for the Calculus of Inductive Constructions. 24:1-24:19 - Andreas Lochbihler:
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. 25:1-25:18 - Marco Maggesi, Cosimo Perini Brogi:
A Formal Proof of Modal Completeness for Provability Logic. 26:1-26:18 - César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, Thiago Mendonça Ferreira Ramos:
Formal Verification of Termination Criteria for First-Order Recursive Functions. 27:1-27:17 - Raja Natarajan, Suneel Sarswat, Abhishek Kr Singh:
Verified Double Sided Auctions for Financial Markets. 28:1-28:18 - Pierre Nigron, Pierre-Évariste Dagand:
Reaching for the Star: Tale of a Monad in Coq. 29:1-29:19 - Konrad Slind:
Specifying Message Formats with Contiguity Types. 30:1-30:17 - Laurent Théry:
Proof Pearl : Playing with the Tower of Hanoi Formally. 31:1-31:16 - Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic:
Verifying an HTTP Key-Value Server with Interaction Trees and VST. 32:1-32:19
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.
last updated on 2025-12-09 23:35 CET 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:
