Program
ITP 2021
All times are in the Central European Summer Timezone (CEST), UTC+2, GMT+2
Talks will be 20 minutes long + 5 minutes for questions
PROGRAM OVERVIEW
All times are in the Central European Summer Timezone (CEST), UTC+2, GMT+2
Talks will be 20 minutes long + 5 minutes for questions
Sessions will be held online using Zoom
Monday – 28th of June
Tuesday – 29th of June
Theory I
10:00 – 11:45
Chair: Matthieu Sozeau
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value λ-Calculus
Yannick Forster, Fabian Kunze, Gert Smolka and Maximilian Wuttke.
Flexible coinduction in Agda
Luca Ciccone, Francesco Dagnino and Elena Zucca.
Reaching for the Star: Tale of a Monad in Coq
Pierre Nigron and Pierre-Evariste Dagand.
Homotopy Type Theory in Isabelle (Short Paper)
Joshua Chen.
Break
11:45 – 12:15
Mathematics Formalizations
12:15 – 13:30
Chair: Larry Paulson
A formalization of Dedekind domains and class groups of global fields
Anne Baanen, Sander R. Dahmen, Filippo A. E. Nuccio Mortarino Majno di Capriglio and Ashvni Narayanan.
Proof Pearl : Playing with the Tower of Hanoi Formally
Laurent Théry.
Formalized Haar Measure.
Floris van Doorn
Break
13:30 – 15:00
Verification 1
15:00 – 16:15
Chair: Tobias Nipkow
Formal Verification of Termination Criteria for First-Order Recursive Functions
Cesar Munoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron Dutle, Anthony Narkawicz, Ariane Alves Almeida, Andreia B. Avelar da Silva and Thiago M. Ferreira Ramos.
A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm
Katherine Cordwell, Yong Kiam Tan and André Platzer
Verifying an HTTP Key-Value Server with Interaction Trees and VST
Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce and Steve Zdancewic
Break
16:15 – 16:45
Invited Talk – Andrei Popescu
16:45 – 17:45
Chair: Tobias Nipkow
Title: Bounded-Deducibility Security
Wednesday – 30th of June
Theory II
10:45 – 12:00
Chair: Claudia Nalon
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq
Dominik Kirst and Marc Hermes.
A formal proof of modal completeness for provability logic
Marco Maggesi and Cosimo Perini Brogi.
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq
Lennard Gäher and Fabian Kunze.
Break
12:00 – 12:30
Verification II
12:30 – 13:45
Chair: Claudio Sacerdoti-Coen
Verified Progress Tracking for Timely Dataflow
Matthias Brun, Sára Decova, Andrea Lattuada and Dmitriy Traytel
Complete Bidirectional Typing for the Calculus of Inductive Constructions
Meven Lennon-Bertrand.
Specifying Message Formats with Contiguity Types
Konrad Slind
Break
13:45 – 15:00
Formalizations I
15:00 – 16:15
Chair: Amy Felty
Proving Quantum Programs Correct
Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li and Michael Hicks.
Formalization of Basic Combinatorics on Words
Stepan Holub and Stepan Starosta
Unsolvability of the Quintic Formalized in Dependent Type Theory
Sophie Bernard, Cyril Cohen, Assia Mahboubi and Pierre-Yves Strub.
Break
16:15 – 16:45
Business Meeting
16:45 – 17:45
Chair: Larry Paulson
Break
17:45 – 18:00
Invited Talk – Nadia Polikarpova
(joint with LICS 2021)
18:00 – 19:00
Chair: Liron Cohen
Title: Synthesis of Safe Pointer-Manipulating Programs
Thursday – 01st of July
Formalizations II
10:00 – 11:45
Chair: Adam Naumowicz
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche
Peter Koepke, Adrian De Lon and Anton Lorenzen
Value-oriented Legal Argumentation in Isabelle/HOL
Christoph Benzmüller and David Fuenmayor
A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps
Christian Doczkal.
Verified Double Sided Auctions for Financial Markets
Raja Natarajan, Suneel Sarswat and Abhishek Kr Singh.
Break
11:45 – 12:15
Automation and extensions of proof assistants
12:15 – 13:30
Chair: Jeremy Avigad
Itauto: an Extensible Intuitionistic SAT Solver
Frédéric Besson.
Syntactic-semantic Form of Mizar Articles
Czesław Byliński, Artur Korniłowicz and Adam Naumowicz.
A graphical user interface framework for formal verification
Edward William Ayers, Mateja Jamnik and William Gowers.
Break
13:30 – 15:00
Formalization III
15:00 – 16:15
Chair: Jeremy Avigad
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks
Andreas Lochbihler
Formalising a Turing-Complete Choreographic Language in Coq
Luís Cruz-Filipe, Fabrizio Montesi and Marco Peressotti
A Formally Verified TESC Verifier
Seulkee Baek
Break
16:15 – 16:45
Invited Talk – Magnus Myreen
16:45 – 17:45
Chair: Cezary Kaliszyk
Title: The CakeML Project’s Quest for Ever Stronger Correctness Theorems