ITP 2022 August 7-10, 2022, Haifa, Israel

13th International Conference on Interactive Theorem Proving (ITP 2022)



June Andronick and Leonardo de Moura (Eds.)
ISBN 978-3-95977-252-5, LIPICS Vol. 237 ISSN 1868-8969
Additional Information
License
Conference Website
Complete volume (PDF, 8 MB)
Search Publication Server

Authors
  • Abrahamsson, Oskar
  • Åman Pohjola, Johannes
  • Andronick, June
  • Baanen, Anne
  • Bapanapally, Jagadish
  • Becker, Heiko
  • Biernacka, Małgorzata
  • Blanchette, Jasmin
  • Charatonik, Witold
  • Chen, Carol
  • Chlipala, Adam
  • Darulova, Eva
  • de Frutos-Fernández, María Inés
  • de Moura, Leonardo
  • Desharnais, Martin
  • Dillies, Yaël
  • Drab, Tomasz
  • Dudenhefner, Andrej
  • Dupuis, Frédéric
  • Edmonds, Chelsea
  • Erbsen, Andres
  • Felty, Amy
  • Forster, Yannick
  • Fox, Anthony C. J.
  • From, Asta Halkjær
  • Gaboardi, Marco
  • Gamboa, Ruben
  • Gengelbach, Arve
  • Goertzel, Zarathustra A.
  • Gómez-Londoño, Alejandro
  • Gross, Jason
  • Hao, Jifeng
  • Hostert, Johannes
  • Jacobsen, Frederik Krogsdal
  • Jakubův, Jan
  • Jeannin, Jean-Baptiste
  • Kaliszyk, Cezary
  • Kanabar, Hrutvik
  • Karayel, Emin
  • Kavvos, G. A.
  • Kirst, Dominik
  • Kudryashov, Yury
  • Kumar, Ramana
  • Kunze, Fabian
  • Lammich, Peter
  • Lampropoulos, Leonidas
  • Lauermann, Nils
  • Lewis, Robert Y.
  • Lv, Yi
  • Macbeth, Heather
  • Magaud, Nicolas
  • Mehta, Bhavik
  • Moss, J. Eliot B.
  • Myreen, Magnus O.
  • Norrish, Michael
  • Olšák, Miroslav
  • Pąk, Karol
  • Paulson, Lawrence C.
  • Pestun, Vasily
  • Philipoom, Jade
  • Piepenbrock, Jelle
  • Poddar-Agrawal, Miraya
  • Pohjola, Johannes Åman
  • Prinz, Jacob
  • Qu, Weihao
  • Sakaguchi, Kazuhiko
  • Sewell, Thomas
  • Shaker, James
  • Shinnar, Avraham
  • Stoughton, Alley
  • Tekriwal, Mohit
  • Thomas, Philip S.
  • Trager, Barry
  • Urban, Josef
  • Vajjha, Koundinya
  • Volkova, Anastasia
  • Vukmirović, Petar
  • Wang, Shuling
  • Wenzel, Makarius
  • Xia, Bican
  • Yeager, Jared
  • Ye, Hong
  • Zhan, Bohua
  • Zhao, Gehang
  • Zimmermann, Théo
    		•

    		  
    Front Matter, Table of Contents, Preface, Conference Organization
    Authors: Andronick, June ; de Moura, Leonardo

    Abstract | Document (457 KB) | BibTeX

    Modelling and Verifying Properties of Biological Neural Networks (Invited Talk)
    Authors: Felty, Amy

    Abstract | Document (416 KB) | BibTeX

    User Interface Design in the HolPy Theorem Prover (Invited Talk)
    Authors: Zhan, Bohua

    Abstract | Document (318 KB) | BibTeX

    Candle: A Verified Implementation of HOL Light
    Authors: Abrahamsson, Oskar ; Myreen, Magnus O. ; Kumar, Ramana ; Sewell, Thomas

    Abstract | Document (634 KB) | BibTeX

    Use and Abuse of Instance Parameters in the Lean Mathematical Library
    Authors: Baanen, Anne

    Abstract | Document (754 KB) | BibTeX

    A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(R)
    Authors: Bapanapally, Jagadish ; Gamboa, Ruben

    Abstract | Document (673 KB) | BibTeX

    Dandelion: Certified Approximations of Elementary Functions
    Authors: Becker, Heiko ; Tekriwal, Mohit ; Darulova, Eva ; Volkova, Anastasia ; Jeannin, Jean-Baptiste

    Abstract | Document (783 KB) | BibTeX

    The Zoo of Lambda-Calculus Reduction Strategies, And Coq
    Authors: Biernacka, Małgorzata ; Charatonik, Witold ; Drab, Tomasz

    Abstract | Document (856 KB) | BibTeX

    Seventeen Provers Under the Hammer
    Authors: Desharnais, Martin ; Vukmirović, Petar ; Blanchette, Jasmin ; Wenzel, Makarius

    Abstract | Document (770 KB) | BibTeX

    Formalising Szemerédi’s Regularity Lemma in Lean
    Authors: Dillies, Yaël ; Mehta, Bhavik

    Abstract | Document (753 KB) | BibTeX

    Formalized functional analysis with semilinear maps
    Authors: Dupuis, Frédéric ; Lewis, Robert Y. ; Macbeth, Heather

    Abstract | Document (866 KB) | BibTeX

    Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
    Authors: Edmonds, Chelsea ; Paulson, Lawrence C.

    Abstract | Document (699 KB) | BibTeX

    Synthetic Kolmogorov Complexity in Coq
    Authors: Forster, Yannick ; Kunze, Fabian ; Lauermann, Nils

    Abstract | Document (804 KB) | BibTeX

    Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
    Authors: From, Asta Halkjær ; Jacobsen, Frederik Krogsdal

    Abstract | Document (746 KB) | BibTeX

    Formalizing the Ring of Adèles of a Global Field
    Authors: de Frutos-Fernández, María Inés

    Abstract | Document (817 KB) | BibTeX

    A Verified Cyclicity Checker: For Theories with Overloaded Constants
    Authors: Gengelbach, Arve ; Åman Pohjola, Johannes

    Abstract | Document (807 KB) | BibTeX

    The Isabelle ENIGMA
    Authors: Goertzel, Zarathustra A. ; Jakubův, Jan ; Kaliszyk, Cezary ; Olšák, Miroslav ; Piepenbrock, Jelle ; Urban, Josef

    Abstract | Document (800 KB) | BibTeX

    Accelerating Verified-Compiler Development with a Verified Rewriting Engine
    Authors: Gross, Jason ; Erbsen, Andres ; Philipoom, Jade ; Poddar-Agrawal, Miraya ; Chlipala, Adam

    Abstract | Document (1,126 KB) | BibTeX

    Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
    Authors: Gross, Jason ; Zimmermann, Théo ; Poddar-Agrawal, Miraya ; Chlipala, Adam

    Abstract | Document (674 KB) | BibTeX

    Undecidability of Dyadic First-Order Logic in Coq
    Authors: Hostert, Johannes ; Dudenhefner, Andrej ; Kirst, Dominik

    Abstract | Document (817 KB) | BibTeX

    Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
    Authors: Kanabar, Hrutvik ; Fox, Anthony C. J. ; Myreen, Magnus O.

    Abstract | Document (798 KB) | BibTeX

    Formalization of Randomized Approximation Algorithms for Frequency Moments
    Authors: Karayel, Emin

    Abstract | Document (972 KB) | BibTeX

    Computational Back-And-Forth Arguments in Constructive Type Theory
    Authors: Kirst, Dominik

    Abstract | Document (753 KB) | BibTeX

    Formalizing the Divergence Theorem and the Cauchy Integral Formula in Lean
    Authors: Kudryashov, Yury

    Abstract | Document (794 KB) | BibTeX

    Refinement of Parallel Algorithms down to LLVM
    Authors: Lammich, Peter

    Abstract | Document (756 KB) | BibTeX

    Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant
    Authors: Magaud, Nicolas

    Abstract | Document (791 KB) | BibTeX

    Formalizing a Diophantine Representation of the Set of Prime Numbers
    Authors: Pąk, Karol ; Kaliszyk, Cezary

    Abstract | Document (730 KB) | BibTeX

    Kalas: A Verified, End-To-End Compiler for a Choreographic Language
    Authors: Pohjola, Johannes Åman ; Gómez-Londoño, Alejandro ; Shaker, James ; Norrish, Michael

    Abstract | Document (948 KB) | BibTeX

    Deeper Shallow Embeddings
    Authors: Prinz, Jacob ; Kavvos, G. A. ; Lampropoulos, Leonidas

    Abstract | Document (617 KB) | BibTeX

    Reflexive Tactics for Algebra, Revisited
    Authors: Sakaguchi, Kazuhiko

    Abstract | Document (846 KB) | BibTeX

    Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
    Authors: Stoughton, Alley ; Chen, Carol ; Gaboardi, Marco ; Qu, Weihao

    Abstract | Document (750 KB) | BibTeX

    Formalization of a Stochastic Approximation Theorem
    Authors: Vajjha, Koundinya ; Trager, Barry ; Shinnar, Avraham ; Pestun, Vasily

    Abstract | Document (903 KB) | BibTeX

    Mechanizing Soundness of Off-Policy Evaluation
    Authors: Yeager, Jared ; Moss, J. Eliot B. ; Norrish, Michael ; Thomas, Philip S.

    Abstract | Document (773 KB) | BibTeX

    Compositional Verification of Interacting Systems Using Event Monads
    Authors: Zhan, Bohua ; Lv, Yi ; Wang, Shuling ; Zhao, Gehang ; Hao, Jifeng ; Ye, Hong ; Xia, Bican

    Abstract | Document (661 KB) | BibTeX

    		  



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