ITP 2023 Program

Invited Speakers:

Angeliki Koutsoukou-Argyraki, University of Cambridge
Robbert Krebbers, Radboud University Nijmegen

Schedule of Sessions and Talks:

Monday, 31 July 2023

09:00-11:00WEPN WorkshopCoq Workshop
11:00-11:30Coffee Break
11:30-13:30WEPN WorkshopCoq Workshop
15:00-16:30Mizar 50 WorkshopCoq Workshop
16:30-17:00Coffee Break
17:00-18:00Mizar 50 WorkshopCoq Workshop

Tuesday, 1 August 2023

08:55-09:00Conference Opening
Invited Talk and Session: Algorithms. Chair: René Thiemann
09:00-10:00Angeliki Koutsoukou-Argyraki: Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)
10:00-10:30Chengsong Tan and Christian Urban: POSIX Lexing with Bitcoded Derivatives
10:30-11:00Balazs Toth and Tobias Nipkow: Real-Time Double-Ended Queue Verified (Proof Pearl)
11:00-11:30Coffee Break
Session: Proof Assistants. Chair: Makarius Wenzel
11:30-12:00Oskar Abrahamsson and Magnus O. Myreen: Fast, Verified Computation for Candle
12:00-12:30Mario Carneiro: Reimplementing Mizar in Rust
12:30-13:00Simon Guilloud, Sankalp Gambhir and Viktor Kuncak: LISA - A Modern Proof System
13:00-13:30Yiming Xu and Michael Norrish: Dependently Sorted Theorem Proving for Mathematical Foundations
Session: Hammers and Machine Learning. Chair: Jeremy Avigad
15:00-15:30Mario Carneiro, Chad Brown and Josef Urban: Automated Theorem Proving for Metamath
15:30-16:00Jan Jakubuv, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Miroslav Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda and Josef Urban: MizAR 60 for Mizar 50
16:00-16:30Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner and Talia Ringer: Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset
16:30-17:00Coffee Break
Session: Rewriting. Chair: Akihisa Yamada
17:00-17:30Niels van der Weide, Deivid Vale and Cynthia Kop: Certifying Higher-Order Polynomial Interpretations
17:30-18:00Christina Kohl and Aart Middeldorp: Formalizing Almost Development Closed Critical Pairs (Short Paper)

Wednesday, 2 August 2023

Invited Talk and Session: Usability. Chair: Adam Naumowicz
09:00-10:00Robbert Krebbers: Interactive and Automated Proofs in Modal Separation Logic (Invited Talk)
10:00-10:30Wojciech Nawrocki, Edward W. Ayers and Gabriel Ebner: An extensible user interface for Lean 4
10:30-11:00Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Erik Martin-Dorel, Karl Palmskog, Alexander Serebrenik and Théo Zimmermann: Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
11:00-11:30Coffee Break
Session: Mathematics - Part 1. Chair: Larry Paulson
11:30-12:00David Kurniadi Angdinata and Junyan Xu: An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in any Characteristic
12:00-12:30María Inés de Frutos-Fernández: Formalizing Norm Extensions and Applications to Number Theory
12:30-13:00Jujian Zhang: Formalising the Proj construction in Lean
13:00-13:30Alex Best, Christopher Birkbeck, Riccardo Brasca and Eric Rodriguez: Fermat’s Last Theorem for regular primes (Short Paper)
14:30-24:00Excursion and Conference Dinner

Thursday, 3 August 2023

Session: Foundations. Chair: Robbert Krebbers
09:00-09:30Roger Bosman, Georgios Karachalias and Tom Schrijvers: No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System
09:30-10:00Lawrence Dunn, Val Tannen and Steve Zdancewic: Tealeaves: Structured monads for generic first-order abstract syntax infrastructure
10:00-10:30Akihisa Yamada and Jérémy Dubut: Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)
10:30-11:00Adam Grabowski and Artur Korniłowicz: Implementing More Explicit Definitional Expansions in Mizar (Short Paper)
11:00-11:30Coffee Break
Session: Models of Computation. Chair: Tobias Nipkow
11:30-12:00Beniamino Accattoli, Horace Blanc and Claudio Sacerdoti Coen: Formalizing Functions as Processes
12:00-12:30Martin Dvorak and Jasmin Blanchette: Closure Properties of General Grammars — Formally Verified
12:30-13:00Michikazu Hirata, Yasuhiko Minamide and Tetsuya Sato: Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL
13:00-13:30Dominique Larchey-Wendling and Jean-Francois Monin: Proof pearl: faithful computation and extraction of µ-recursive algorithms in Coq
Session: Compiler and Interpreter. Chair: Magnus Myreen
15:00-15:30Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer and Alon Titelman: A Proof-Producing Compiler for Blockchain Applications
15:30-16:00Luís Cruz-Filipe and Fabrizio Montesi: Now It Compiles!: Certified Automatic Repair of Uncompilable Protocols
16:00-16:30Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer and Andrew W. Appel: Foundational verification of stateful P4 packet processing
16:30-17:00Coffee Break
17:00-18:00Business Meeting. Chair: Larry Paulson

Friday, 4 August 2023

Session: Category and Type Theory. Chair: Claudio Sacerdoti Coen
09:00-09:30Jarl G. Taxeraas Flaten: Formalising Yoneda Ext in Univalent Foundations
09:30-10:00Philipp Joram and Niccolò Veltri: Constructive Final Semantics of Finite Bags
10:00-10:30Dawit Tirore, Jesper Bengtson and Marco Carbone: A Sound and Complete Projection for Global Types
10:30-11:00Niels Voorneveld: Slice Nondeterminism
11:00-11:30Coffee Break
Session: Mathematics - Part 2. Chair: Josef Urban
11:30-12:00Mohammad Abdulaziz and Christoph Madlener: A Formal Analysis of RANKING
12:00-12:30Amelia Livingston: Group cohomology in the Lean community library
12:30-13:00Oliver Nash: A formalisation of Gallagher’s ergodic theorem
13:00-13:30Pierre Pomeret-Coquot, Helene Fargier and Érik Martin-Dorel: Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant

If you have any problems or questions, please contact us via e-mail at: