Invited Speakers:

Schedule of Sessions and Talks:

Monday, 31 July 2023

08:30-09:00	Registration
09:00-11:00	WEPN Workshop	Coq Workshop
11:00-11:30	Coffee Break
11:30-13:30	WEPN Workshop	Coq Workshop
13:30-15:00	Lunch
15:00-16:30	Mizar 50 Workshop	Coq Workshop
16:30-17:00	Coffee Break
17:00-18:00	Mizar 50 Workshop	Coq Workshop

Tuesday, 1 August 2023

08:30-08:55	Registration
08:55-09:00	Conference Opening
Invited Talk and Session: Algorithms. Chair: René Thiemann
09:00-10:00	Angeliki Koutsoukou-Argyraki: Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)
10:00-10:30	Chengsong Tan and Christian Urban: POSIX Lexing with Bitcoded Derivatives
10:30-11:00	Balazs Toth and Tobias Nipkow: Real-Time Double-Ended Queue Verified (Proof Pearl)
11:00-11:30	Coffee Break
Session: Proof Assistants. Chair: Makarius Wenzel
11:30-12:00	Oskar Abrahamsson and Magnus O. Myreen: Fast, Verified Computation for Candle
12:00-12:30	Mario Carneiro: Reimplementing Mizar in Rust
12:30-13:00	Simon Guilloud, Sankalp Gambhir and Viktor Kuncak: LISA - A Modern Proof System
13:00-13:30	Yiming Xu and Michael Norrish: Dependently Sorted Theorem Proving for Mathematical Foundations
13:30-15:00	Lunch
Session: Hammers and Machine Learning. Chair: Jeremy Avigad
15:00-15:30	Mario Carneiro, Chad Brown and Josef Urban: Automated Theorem Proving for Metamath
15:30-16:00	Jan 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:30	Tom 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:00	Coffee Break
Session: Rewriting. Chair: Akihisa Yamada
17:00-17:30	Niels van der Weide, Deivid Vale and Cynthia Kop: Certifying Higher-Order Polynomial Interpretations
17:30-18:00	Christina Kohl and Aart Middeldorp: Formalizing Almost Development Closed Critical Pairs (Short Paper)

Wednesday, 2 August 2023

08:45-09:00	Registration
Invited Talk and Session: Usability. Chair: Adam Naumowicz
09:00-10:00	Robbert Krebbers: Interactive and Automated Proofs in Modal Separation Logic (Invited Talk)
10:00-10:30	Wojciech Nawrocki, Edward W. Ayers and Gabriel Ebner: An extensible user interface for Lean 4
10:30-11:00	Ana 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:30	Coffee Break
Session: Mathematics - Part 1. Chair: Larry Paulson
11:30-12:00	David Kurniadi Angdinata and Junyan Xu: An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in any Characteristic
12:00-12:30	María Inés de Frutos-Fernández: Formalizing Norm Extensions and Applications to Number Theory
12:30-13:00	Jujian Zhang: Formalising the Proj construction in Lean
13:00-13:30	Alex Best, Christopher Birkbeck, Riccardo Brasca and Eric Rodriguez: Fermat’s Last Theorem for regular primes (Short Paper)
13:30-14:30	Lunch
14:30-24:00	Excursion and Conference Dinner

Thursday, 3 August 2023

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

Friday, 4 August 2023

08:45-09:00	Registration
Session: Category and Type Theory. Chair: Claudio Sacerdoti Coen
09:00-09:30	Jarl G. Taxeraas Flaten: Formalising Yoneda Ext in Univalent Foundations
09:30-10:00	Philipp Joram and Niccolò Veltri: Constructive Final Semantics of Finite Bags
10:00-10:30	Dawit Tirore, Jesper Bengtson and Marco Carbone: A Sound and Complete Projection for Global Types
10:30-11:00	Niels Voorneveld: Slice Nondeterminism
11:00-11:30	Coffee Break
Session: Mathematics - Part 2. Chair: Josef Urban
11:30-12:00	Mohammad Abdulaziz and Christoph Madlener: A Formal Analysis of RANKING
12:00-12:30	Amelia Livingston: Group cohomology in the Lean community library
12:30-13:00	Oliver Nash: A formalisation of Gallagher’s ergodic theorem
13:00-13:30	Pierre 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
13:30-15:00	Lunch