ITP 2023 Program

Invited Speakers:

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

List of Accepted Papers:

  • Mohammad Abdulaziz and Christoph Madlener: A Formal Analysis of RANKING
  • Oliver Nash: A formalisation of Gallagher’s ergodic theorem
  • Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer and Alon Titelman: A Proof-Producing Compiler for Blockchain Applications
  • Dawit Tirore, Jesper Bengtson and Marco Carbone: A Sound and Complete Projection for Global Types
  • David Kurniadi Angdinata and Junyan Xu: An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in any Characteristic
  • Wojciech Nawrocki, Edward W. Ayers and Gabriel Ebner: An extensible user interface for Lean 4
  • Mario Carneiro, Chad Brown and Josef Urban: Automated Theorem Proving for Metamath
  • 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
  • Niels van der Weide, Deivid Vale and Cynthia Kop: Certifying Higher-Order Polynomial Interpretations
  • Martin Dvorak and Jasmin Blanchette: Closure Properties of Unrestricted Grammars — Formally Verified
  • Philipp Joram and Niccolò Veltri: Constructive Final Semantics of Finite Bags
  • Yiming Xu and Michael Norrish: Dependent Sorted Theorem Proving for Mathematical Foundations
  • Oskar Abrahamsson and Magnus O. Myreen: Fast, Verified Computation for Candle
  • Alex Best, Christopher Birkbeck, Riccardo Brasca and Eric Rodriguez: Fermat’s Last Theorem for regular primes (short paper)
  • Jujian Zhang: Formalising the Proj construction
  • Jarl G. Taxeraas Flaten: Formalising Yoneda Ext in Univalent Foundations
  • Christina Kohl and Aart Middeldorp: Formalizing Almost Development Closed Critical Pairs (Short Paper)
  • Beniamino Accattoli, Horace Blanc and Claudio Sacerdoti Coen: Formalizing Functions as Processes
  • María Inés de Frutos-Fernández: Formalizing Norm Extensions and Applications to Number Theory
  • Akihisa Yamada and Jérémy Dubut: Formalizing Results on Directed Sets in Isabelle/HOL
  • Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer and Andrew W. Appel: Foundational verification of stateful P4 packet processing
  • Amelia Livingston: Group cohomology in the Lean community library
  • Adam Grabowski and Artur Korniłowicz: Implementing More Explicit Definitional Expansions in Mizar (short paper)
  • 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
  • Simon Guilloud, Sankalp Gambhir and Viktor Kuncak: LISA - A Proof Assistant Embedded in Scala
  • 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
  • Roger Bosman, Georgios Karachalias and Tom Schrijvers: No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System
  • Luís Cruz-Filipe and Fabrizio Montesi: Now It Compiles! - Certified Automatic Repair of Uncompilable Protocols
  • Chengsong Tan and Christian Urban: POSIX Lexing with Bitcoded Derivatives
  • Dominique Larchey-Wendling and Jean-Francois Monin: Proof pearl: faithful computation and extraction of µ-recursive algorithms in Coq
  • Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner and Talia Ringer: Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset
  • Balazs Toth and Tobias Nipkow: Real-Time Double-Ended Queue Verified (Proof Pearl)
  • Mario Carneiro: Reimplementing Mizar in Rust
  • Michikazu Hirata, Yasuhiko Minamide and Tetsuya Sato: Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL
  • Niels Voorneveld: Slice Nondeterminism
  • Lawrence Dunn, Val Tannen and Steve Zdancewic: Tealeaves: Structured monads for generic first-order abstract syntax infrastructure

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