LIPIcs, Volume 268, ITP 2023

• Adam Naumowicz and René Thiemann LIPIcs, Volume 268, ITP 2023, Complete Volume 10.4230/LIPIcs.ITP.2023
• Adam Naumowicz and René Thiemann Front Matter, Table of Contents, Preface, Conference Organization 10.4230/LIPIcs.ITP.2023.0
• Angeliki Koutsoukou-Argyraki Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk) 10.4230/LIPIcs.ITP.2023.1
• Robbert Krebbers Interactive and Automated Proofs in Modal Separation Logic (Invited Talk) 10.4230/LIPIcs.ITP.2023.2
• Mohammad Abdulaziz and Christoph Madlener A Formal Analysis of RANKING 10.4230/LIPIcs.ITP.2023.3
• Oskar Abrahamsson and Magnus O. Myreen Fast, Verified Computation for Candle 10.4230/LIPIcs.ITP.2023.4
• Beniamino Accattoli, Horace Blanc, and Claudio Sacerdoti Coen Formalizing Functions as Processes 10.4230/LIPIcs.ITP.2023.5
• David Kurniadi Angdinata and Junyan Xu An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic 10.4230/LIPIcs.ITP.2023.6
• Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman A Proof-Producing Compiler for Blockchain Applications 10.4230/LIPIcs.ITP.2023.7
• Roger Bosman, Georgios Karachalias, and Tom Schrijvers No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System 10.4230/LIPIcs.ITP.2023.8
• Mario Carneiro, Chad E. Brown, and Josef Urban Automated Theorem Proving for Metamath 10.4230/LIPIcs.ITP.2023.9
• Mario Carneiro Reimplementing Mizar in Rust 10.4230/LIPIcs.ITP.2023.10
• Luís Cruz-Filipe and Fabrizio Montesi Now It Compiles! Certified Automatic Repair of Uncompilable Protocols 10.4230/LIPIcs.ITP.2023.11
• Ana de Almeida Borges, Annalí Casanueva Artís, Jean-Rémy Falleri, Emilio Jesús Gallego Arias, Érik Martin-Dorel, Karl Palmskog, Alexander Serebrenik, and Théo Zimmermann Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users 10.4230/LIPIcs.ITP.2023.12
• María Inés de Frutos-Fernández Formalizing Norm Extensions and Applications to Number Theory 10.4230/LIPIcs.ITP.2023.13
• Lawrence Dunn, Val Tannen, and Steve Zdancewic Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure 10.4230/LIPIcs.ITP.2023.14
• Martin Dvorak and Jasmin Blanchette Closure Properties of General Grammars – Formally Verified 10.4230/LIPIcs.ITP.2023.15
• Jarl G. Taxerås Flaten Formalising Yoneda Ext in Univalent Foundations 10.4230/LIPIcs.ITP.2023.16
• Simon Guilloud, Sankalp Gambhir, and Viktor Kunčak LISA - A Modern Proof System 10.4230/LIPIcs.ITP.2023.17
• Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL 10.4230/LIPIcs.ITP.2023.18
• Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, and Josef Urban MizAR 60 for Mizar 50 10.4230/LIPIcs.ITP.2023.19
• Philipp Joram and Niccolò Veltri Constructive Final Semantics of Finite Bags 10.4230/LIPIcs.ITP.2023.20
• Dominique Larchey-Wendling and Jean-François Monin Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq 10.4230/LIPIcs.ITP.2023.21
• Amelia Livingston Group Cohomology in the Lean Community Library 10.4230/LIPIcs.ITP.2023.22
• Oliver Nash A Formalisation of Gallagher’s Ergodic Theorem 10.4230/LIPIcs.ITP.2023.23
• Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner An Extensible User Interface for Lean 4 10.4230/LIPIcs.ITP.2023.24
• Pierre Pomeret-Coquot, Hélène Fargier, and Érik Martin-Dorel Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant 10.4230/LIPIcs.ITP.2023.25
• Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset 10.4230/LIPIcs.ITP.2023.26
• Chengsong Tan and Christian Urban POSIX Lexing with Bitcoded Derivatives 10.4230/LIPIcs.ITP.2023.27
• Dawit Tirore, Jesper Bengtson, and Marco Carbone A Sound and Complete Projection for Global Types 10.4230/LIPIcs.ITP.2023.28
• Balazs Toth and Tobias Nipkow Real-Time Double-Ended Queue Verified (Proof Pearl) 10.4230/LIPIcs.ITP.2023.29
• Niels van der Weide, Deivid Vale, and Cynthia Kop Certifying Higher-Order Polynomial Interpretations 10.4230/LIPIcs.ITP.2023.30
• Niels F. W. Voorneveld Slice Nondeterminism 10.4230/LIPIcs.ITP.2023.31
• Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, and Andrew W. Appel Foundational Verification of Stateful P4 Packet Processing 10.4230/LIPIcs.ITP.2023.32
• Yiming Xu and Michael Norrish Dependently Sorted Theorem Proving for Mathematical Foundations 10.4230/LIPIcs.ITP.2023.33
• Akihisa Yamada and Jérémy Dubut Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl) 10.4230/LIPIcs.ITP.2023.34
• Jujian Zhang Formalising the Proj Construction in Lean 10.4230/LIPIcs.ITP.2023.35
• Alex J. Best, Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi Fermat’s Last Theorem for Regular Primes (Short Paper) 10.4230/LIPIcs.ITP.2023.36
• Adam Grabowski and Artur Korniłowicz Implementing More Explicit Definitional Expansions in Mizar (Short Paper) 10.4230/LIPIcs.ITP.2023.37
• Christina Kohl and Aart Middeldorp Formalizing Almost Development Closed Critical Pairs (Short Paper) 10.4230/LIPIcs.ITP.2023.38