ITP 2023 Program
Invited Speakers:
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
Contact
If you have any problems or questions, please contact us via e-mail at:
itp2023@mizar.uwb.edu.pl