ITP 2023 July 31 to August 4, 2023, Białystok, Poland

14th International Conference on Interactive Theorem Proving (ITP 2023)



Adam Naumowicz and René Thiemann (Eds.)
ISBN 978-3-95977-284-6, LIPICS Vol. 268 ISSN 1868-8969
Additional Information
License
Conference Website
Complete volume (PDF, 10 MB)
Search Publication Server

Authors
  • Abdulaziz, Mohammad
  • Abrahamsson, Oskar
  • Accattoli, Beniamino
  • Angdinata, David Kurniadi
  • Appel, Andrew W.
  • Avigad, Jeremy
  • Ayers, Edward W.
  • Bengtson, Jesper
  • Beringer, Lennart
  • Best, Alex J.
  • Birkbeck, Christopher
  • Blanchette, Jasmin
  • Blanc, Horace
  • Bosman, Roger
  • Brasca, Riccardo
  • Brown, Chad E.
  • Carbone, Marco
  • Carneiro, Mario
  • Casanueva Artís, Annalí
  • Chvalovský, Karel
  • Cruz-Filipe, Luís
  • de Almeida Borges, Ana
  • de Frutos-Fernández, María Inés
  • Doenges, Ryan
  • Dubut, Jérémy
  • Dunn, Lawrence
  • Dvorak, Martin
  • Ebner, Gabriel
  • Falleri, Jean-Rémy
  • Fargier, Hélène
  • Flaten, Jarl G. Taxerås
  • Gallego Arias, Emilio Jesús
  • Gambhir, Sankalp
  • Gardner, Andrew
  • Goertzel, Zarathustra
  • Goldberg, Lior
  • Grabowski, Adam
  • Guilloud, Simon
  • Henderson, R. Wesley
  • Hirata, Michikazu
  • Jakubův, Jan
  • Joram, Philipp
  • Kaliszyk, Cezary
  • Karachalias, Georgios
  • Kohl, Christina
  • Kop, Cynthia
  • Korniłowicz, Artur
  • Koutsoukou-Argyraki, Angeliki
  • Krebbers, Robbert
  • Kunčak, Viktor
  • Larchey-Wendling, Dominique
  • Levit, David
  • Livingston, Amelia
  • Madlener, Christoph
  • Martin-Dorel, Érik
  • Middeldorp, Aart
  • Minamide, Yasuhiko
  • Monin, Jean-François
  • Montesi, Fabrizio
  • Myreen, Magnus O.
  • Nash, Oliver
  • Naumowicz, Adam
  • Nawrocki, Wojciech
  • Nipkow, Tobias
  • Norrish, Michael
  • Olšák, Mirek
  • Palmskog, Karl
  • Pan, Mengying
  • Piotrowski, Bartosz
  • Pomeret-Coquot, Pierre
  • Reichel, Tom
  • Ringer, Talia
  • Rodriguez Boidi, Eric
  • Sacerdoti Coen, Claudio
  • Sato, Tetsuya
  • Schrijvers, Tom
  • Schulz, Stephan
  • Seginer, Yoav
  • Serebrenik, Alexander
  • Suda, Martin
  • Tan, Chengsong
  • Tannen, Val
  • Thiemann, René
  • Tirore, Dawit
  • Titelman, Alon
  • Toth, Balazs
  • Touchet, Andrew
  • Urban, Christian
  • Urban, Josef
  • Vale, Deivid
  • van der Weide, Niels
  • Veltri, Niccolò
  • Voorneveld, Niels F. W.
  • Wang, Qinshi
  • Wang, Shengyi
  • Xu, Junyan
  • Xu, Yiming
  • Yamada, Akihisa
  • Zdancewic, Steve
  • Zhang, Jujian
  • Zimmermann, Théo
    		•

    		  
    Front Matter, Table of Contents, Preface, Conference Organization
    Authors: Naumowicz, Adam ; Thiemann, René

    Abstract | Document (490 KB) | BibTeX

    Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)
    Authors: Koutsoukou-Argyraki, Angeliki

    Abstract | Document (439 KB) | BibTeX

    Interactive and Automated Proofs in Modal Separation Logic (Invited Talk)
    Authors: Krebbers, Robbert

    Abstract | Document (347 KB) | BibTeX

    A Formal Analysis of RANKING
    Authors: Abdulaziz, Mohammad ; Madlener, Christoph

    Abstract | Document (926 KB) | BibTeX

    Fast, Verified Computation for Candle
    Authors: Abrahamsson, Oskar ; Myreen, Magnus O.

    Abstract | Document (700 KB) | BibTeX

    Formalizing Functions as Processes
    Authors: Accattoli, Beniamino ; Blanc, Horace ; Sacerdoti Coen, Claudio

    Abstract | Document (815 KB) | BibTeX

    An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic
    Authors: Angdinata, David Kurniadi ; Xu, Junyan

    Abstract | Document (828 KB) | BibTeX

    A Proof-Producing Compiler for Blockchain Applications
    Authors: Avigad, Jeremy ; Goldberg, Lior ; Levit, David ; Seginer, Yoav ; Titelman, Alon

    Abstract | Document (656 KB) | BibTeX

    No Unification Variable Left Behind: Fully Grounding Type Inference for the HDM System
    Authors: Bosman, Roger ; Karachalias, Georgios ; Schrijvers, Tom

    Abstract | Document (844 KB) | BibTeX

    Automated Theorem Proving for Metamath
    Authors: Carneiro, Mario ; Brown, Chad E. ; Urban, Josef

    Abstract | Document (772 KB) | BibTeX

    Reimplementing Mizar in Rust
    Authors: Carneiro, Mario

    Abstract | Document (824 KB) | BibTeX

    Now It Compiles! Certified Automatic Repair of Uncompilable Protocols
    Authors: Cruz-Filipe, Luís ; Montesi, Fabrizio

    Abstract | Document (719 KB) | BibTeX

    Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
    Authors: de Almeida Borges, Ana ; Casanueva Artís, Annalí ; Falleri, Jean-Rémy ; Gallego Arias, Emilio Jesús ; Martin-Dorel, Érik ; Palmskog, Karl ; Serebrenik, Alexander ; Zimmermann, Théo

    Abstract | Document (1,039 KB) | BibTeX

    Formalizing Norm Extensions and Applications to Number Theory
    Authors: de Frutos-Fernández, María Inés

    Abstract | Document (792 KB) | BibTeX

    Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure
    Authors: Dunn, Lawrence ; Tannen, Val ; Zdancewic, Steve

    Abstract | Document (1,097 KB) | BibTeX

    Closure Properties of General Grammars – Formally Verified
    Authors: Dvorak, Martin ; Blanchette, Jasmin

    Abstract | Document (699 KB) | BibTeX

    Formalising Yoneda Ext in Univalent Foundations
    Authors: Flaten, Jarl G. Taxerås

    Abstract | Document (818 KB) | BibTeX

    LISA - A Modern Proof System
    Authors: Guilloud, Simon ; Gambhir, Sankalp ; Kunčak, Viktor

    Abstract | Document (802 KB) | BibTeX

    Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL
    Authors: Hirata, Michikazu ; Minamide, Yasuhiko ; Sato, Tetsuya

    Abstract | Document (838 KB) | BibTeX

    MizAR 60 for Mizar 50
    Authors: Jakubův, Jan ; Chvalovský, Karel ; Goertzel, Zarathustra ; Kaliszyk, Cezary ; Olšák, Mirek ; Piotrowski, Bartosz ; Schulz, Stephan ; Suda, Martin ; Urban, Josef

    Abstract | Document (936 KB) | BibTeX

    Constructive Final Semantics of Finite Bags
    Authors: Joram, Philipp ; Veltri, Niccolò

    Abstract | Document (848 KB) | BibTeX

    Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq
    Authors: Larchey-Wendling, Dominique ; Monin, Jean-François

    Abstract | Document (673 KB) | BibTeX

    Group Cohomology in the Lean Community Library
    Authors: Livingston, Amelia

    Abstract | Document (724 KB) | BibTeX

    A Formalisation of Gallagher’s Ergodic Theorem
    Authors: Nash, Oliver

    Abstract | Document (815 KB) | BibTeX

    An Extensible User Interface for Lean 4
    Authors: Nawrocki, Wojciech ; Ayers, Edward W. ; Ebner, Gabriel

    Abstract | Document (1,496 KB) | BibTeX

    Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant
    Authors: Pomeret-Coquot, Pierre ; Fargier, Hélène ; Martin-Dorel, Érik

    Abstract | Document (945 KB) | BibTeX

    Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset
    Authors: Reichel, Tom ; Henderson, R. Wesley ; Touchet, Andrew ; Gardner, Andrew ; Ringer, Talia

    Abstract | Document (701 KB) | BibTeX

    POSIX Lexing with Bitcoded Derivatives
    Authors: Tan, Chengsong ; Urban, Christian

    Abstract | Document (725 KB) | BibTeX

    A Sound and Complete Projection for Global Types
    Authors: Tirore, Dawit ; Bengtson, Jesper ; Carbone, Marco

    Abstract | Document (906 KB) | BibTeX

    Real-Time Double-Ended Queue Verified (Proof Pearl)
    Authors: Toth, Balazs ; Nipkow, Tobias

    Abstract | Document (645 KB) | BibTeX

    Certifying Higher-Order Polynomial Interpretations
    Authors: van der Weide, Niels ; Vale, Deivid ; Kop, Cynthia

    Abstract | Document (1,038 KB) | BibTeX

    Slice Nondeterminism
    Authors: Voorneveld, Niels F. W.

    Abstract | Document (827 KB) | BibTeX

    Foundational Verification of Stateful P4 Packet Processing
    Authors: Wang, Qinshi ; Pan, Mengying ; Wang, Shengyi ; Doenges, Ryan ; Beringer, Lennart ; Appel, Andrew W.

    Abstract | Document (882 KB) | BibTeX

    Dependently Sorted Theorem Proving for Mathematical Foundations
    Authors: Xu, Yiming ; Norrish, Michael

    Abstract | Document (793 KB) | BibTeX

    Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)
    Authors: Yamada, Akihisa ; Dubut, Jérémy

    Abstract | Document (773 KB) | BibTeX

    Formalising the Proj Construction in Lean
    Authors: Zhang, Jujian

    Abstract | Document (897 KB) | BibTeX

    Fermat’s Last Theorem for Regular Primes (Short Paper)
    Authors: Best, Alex J. ; Birkbeck, Christopher ; Brasca, Riccardo ; Rodriguez Boidi, Eric

    Abstract | Document (654 KB) | BibTeX

    Implementing More Explicit Definitional Expansions in Mizar (Short Paper)
    Authors: Grabowski, Adam ; Korniłowicz, Artur

    Abstract | Document (703 KB) | BibTeX

    Formalizing Almost Development Closed Critical Pairs (Short Paper)
    Authors: Kohl, Christina ; Middeldorp, Aart

    Abstract | Document (712 KB) | BibTeX

    		  



    DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI