- 2021
- Andrei Popescu, Thomas Bauereiss, Peter Lammich:
Bounded-Deducibility Security (Invited Paper). ITP 2021: 3:1-3:20 - Matthias Brun, Sára Decova, Andrea Lattuada
, Dmitriy Traytel:
Verified Progress Tracking for Timely Dataflow. ITP 2021: 10:1-10:20 - Yannick Forster, Fabian Kunze, Gert Smolka, Maxi Wuttke:
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. ITP 2021: 19:1-19:20 - Edward W. Ayers, Mateja Jamnik, William T. Gowers:
A Graphical User Interface Framework for Formal Verification. ITP 2021: 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. ITP 2021: 5:1-5:19 - Seulkee Baek:
A Formally Verified Checker for First-Order Proofs. ITP 2021: 6:1-6:13 - Christoph Benzmüller, David Fuenmayor:
Value-Oriented Legal Argumentation in Isabelle/HOL. ITP 2021: 7:1-7:20 - Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub:
Unsolvability of the Quintic Formalized in Dependent Type Theory. ITP 2021: 8:1-8:18 - Frédéric Besson:
Itauto: An Extensible Intuitionistic SAT Solver. ITP 2021: 9:1-9:18 - Czeslaw Bylinski, Artur Kornilowicz, Adam Naumowicz:
Syntactic-Semantic Form of Mizar Articles. ITP 2021: 11:1-11:17 - Joshua Chen:
Homotopy Type Theory in Isabelle. ITP 2021: 12:1-12:8 - Luca Ciccone, Francesco Dagnino, Elena Zucca:
Flexible Coinduction in Agda. ITP 2021: 13:1-13:19 - Katherine Cordwell, Yong Kiam Tan, André Platzer:
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. ITP 2021: 14:1-14:20 - Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti:
Formalising a Turing-Complete Choreographic Language in Coq. ITP 2021: 15:1-15:18 - Christian Doczkal:
A Variant of Wagner's Theorem Based on Combinatorial Hypermaps. ITP 2021: 17:1-17:17 - Floris van Doorn:
Formalized Haar Measure. ITP 2021: 18:1-18:17 - Lennard Gäher, Fabian Kunze:
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. ITP 2021: 20:1-20:18 - Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks:
Proving Quantum Programs Correct. ITP 2021: 21:1-21:19 - Stepan Holub, Stepán Starosta:
Formalization of Basic Combinatorics on Words. ITP 2021: 22:1-22:17 - Dominik Kirst, Marc Hermes:
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. ITP 2021: 23:1-23:20 - Meven Lennon-Bertrand:
Complete Bidirectional Typing for the Calculus of Inductive Constructions. ITP 2021: 24:1-24:19 - Andreas Lochbihler:
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks. ITP 2021: 25:1-25:18 - Adrian De Lon, Peter Koepke, Anton Lorenzen:
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche. ITP 2021: 16:1-16:11 - Marco Maggesi, Cosimo Perini Brogi:
A Formal Proof of Modal Completeness for Provability Logic. ITP 2021: 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. ITP 2021: 27:1-27:17 - Magnus O. Myreen:
The CakeML Project's Quest for Ever Stronger Correctness Theorems (Invited Paper). ITP 2021: 1:1-1:10 - Raja Natarajan, Suneel Sarswat, Abhishek Kr Singh:
Verified Double Sided Auctions for Financial Markets. ITP 2021: 28:1-28:18 - Pierre Nigron, Pierre-Évariste Dagand:
Reaching for the Star: Tale of a Monad in Coq. ITP 2021: 29:1-29:19 - Nadia Polikarpova:
Synthesis of Safe Pointer-Manipulating Programs (Invited Talk). ITP 2021: 2:1-2:1 - Konrad Slind:
Specifying Message Formats with Contiguity Types. ITP 2021: 30:1-30:17
