ITP 2021 June 29 to July 1, 2021, Rome, Italy (Virtual Conference)

12th International Conference on Interactive Theorem Proving (ITP 2021)



Liron Cohen and Cezary Kaliszyk (Eds.)
ISBN 978-3-95977-188-7, LIPICS Vol. 193 ISSN 1868-8969
Additional Information
License
Conference Website
Complete volume (PDF, 12 MB)
Search Publication Server

Authors
  • Almeida, Ariane A.
  • Avelar, Andréia B.
  • Ayala-Rincón, Mauricio
  • Ayers, Edward W.
  • Baanen, Anne
  • Baek, Seulkee
  • Bauereiss, Thomas
  • Benzmüller, Christoph
  • Beringer, Lennart
  • Bernard, Sophie
  • Besson, Frédéric
  • Brun, Matthias
  • Byliński, Czesław
  • Chen, Joshua
  • Ciccone, Luca
  • Cohen, Cyril
  • Cohen, Liron
  • Cordwell, Katherine
  • Cruz-Filipe, Luís
  • Dagand, Pierre-Évariste
  • Dagnino, Francesco
  • Dahmen, Sander R.
  • Decova, Sára
  • De Lon, Adrian
  • Doczkal, Christian
  • Dutle, Aaron M.
  • Forster, Yannick
  • Fuenmayor, David
  • Gäher, Lennard
  • Gowers, W. T.
  • Hermes, Marc
  • Hicks, Michael
  • Hietala, Kesha
  • Holub, Štěpán
  • Honoré, Wolf
  • Hung, Shih-Han
  • Jamnik, Mateja
  • Kaliszyk, Cezary
  • Kirst, Dominik
  • Koepke, Peter
  • Koh, Nicolas
  • Korniłowicz, Artur
  • Kunze, Fabian
  • Lammich, Peter
  • Lattuada, Andrea
  • Lennon-Bertrand, Meven
  • Li, Liyi
  • Li, Yao
  • Li, Yishuai
  • Lochbihler, Andreas
  • Lorenzen, Anton
  • Maggesi, Marco
  • Mahboubi, Assia
  • Mansky, William
  • M. Ferreira Ramos, Thiago
  • Montesi, Fabrizio
  • Moscato, Mariano M.
  • Muñoz, Cesar A.
  • Myreen, Magnus O.
  • Narayanan, Ashvni
  • Narkawicz, Anthony J.
  • Natarajan, Raja
  • Naumowicz, Adam
  • Nigron, Pierre
  • Nuccio Mortarino Majno di Capriglio, Filippo A. E.
  • Peressotti, Marco
  • Perini Brogi, Cosimo
  • Pierce, Benjamin
  • Platzer, André
  • Polikarpova, Nadia
  • Popescu, Andrei
  • Rand, Robert
  • Sarswat, Suneel
  • Singh, Abhishek Kr
  • Slind, Konrad
  • Smolka, Gert
  • Starosta, Štěpán
  • Strub, Pierre-Yves
  • Tan, Yong Kiam
  • Théry, Laurent
  • Traytel, Dmitriy
  • van Doorn, Floris
  • Wuttke, Maximilian
  • Xia, Li-Yao
  • Zdancewic, Steve
  • Zhang, Hengchu
  • Zucca, Elena
    		•

    		  
    Front Matter, Table of Contents, Preface, Conference Organization
    Authors: Cohen, Liron ; Kaliszyk, Cezary

    Abstract | Document (443 KB) | BibTeX

    The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper)
    Authors: Myreen, Magnus O.

    Abstract | Document (531 KB) | BibTeX

    Synthesis of Safe Pointer-Manipulating Programs (Invited Talk)
    Authors: Polikarpova, Nadia

    Abstract | Document (355 KB) | BibTeX

    Bounded-Deducibility Security (Invited Paper)
    Authors: Popescu, Andrei ; Bauereiss, Thomas ; Lammich, Peter

    Abstract | Document (828 KB) | BibTeX

    A Graphical User Interface Framework for Formal Verification
    Authors: Ayers, Edward W. ; Jamnik, Mateja ; Gowers, W. T.

    Abstract | Document (1,481 KB) | BibTeX

    A Formalization of Dedekind Domains and Class Groups of Global Fields
    Authors: Baanen, Anne ; Dahmen, Sander R. ; Narayanan, Ashvni ; Nuccio Mortarino Majno di Capriglio, Filippo A. E.

    Abstract | Document (775 KB) | BibTeX

    A Formally Verified Checker for First-Order Proofs
    Authors: Baek, Seulkee

    Abstract | Document (660 KB) | BibTeX

    Value-Oriented Legal Argumentation in Isabelle/HOL
    Authors: Benzmüller, Christoph ; Fuenmayor, David

    Abstract | Document (2,455 KB) | BibTeX

    Unsolvability of the Quintic Formalized in Dependent Type Theory
    Authors: Bernard, Sophie ; Cohen, Cyril ; Mahboubi, Assia ; Strub, Pierre-Yves

    Abstract | Document (843 KB) | BibTeX

    Itauto: An Extensible Intuitionistic SAT Solver
    Authors: Besson, Frédéric

    Abstract | Document (773 KB) | BibTeX

    Verified Progress Tracking for Timely Dataflow
    Authors: Brun, Matthias ; Decova, Sára ; Lattuada, Andrea ; Traytel, Dmitriy

    Abstract | Document (781 KB) | BibTeX

    Syntactic-Semantic Form of Mizar Articles
    Authors: Byliński, Czesław ; Korniłowicz, Artur ; Naumowicz, Adam

    Abstract | Document (693 KB) | BibTeX

    Homotopy Type Theory in Isabelle
    Authors: Chen, Joshua

    Abstract | Document (675 KB) | BibTeX

    Flexible Coinduction in Agda
    Authors: Ciccone, Luca ; Dagnino, Francesco ; Zucca, Elena

    Abstract | Document (810 KB) | BibTeX

    A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm
    Authors: Cordwell, Katherine ; Tan, Yong Kiam ; Platzer, André

    Abstract | Document (1,108 KB) | BibTeX

    Formalising a Turing-Complete Choreographic Language in Coq
    Authors: Cruz-Filipe, Luís ; Montesi, Fabrizio ; Peressotti, Marco

    Abstract | Document (654 KB) | BibTeX

    A Natural Formalization of the Mutilated Checkerboard Problem in Naproche
    Authors: De Lon, Adrian ; Koepke, Peter ; Lorenzen, Anton

    Abstract | Document (621 KB) | BibTeX

    A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps
    Authors: Doczkal, Christian

    Abstract | Document (701 KB) | BibTeX

    Formalized Haar Measure
    Authors: van Doorn, Floris

    Abstract | Document (833 KB) | BibTeX

    A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus
    Authors: Forster, Yannick ; Kunze, Fabian ; Smolka, Gert ; Wuttke, Maximilian

    Abstract | Document (1,002 KB) | BibTeX

    Mechanising Complexity Theory: The Cook-Levin Theorem in Coq
    Authors: Gäher, Lennard ; Kunze, Fabian

    Abstract | Document (859 KB) | BibTeX

    Proving Quantum Programs Correct
    Authors: Hietala, Kesha ; Rand, Robert ; Hung, Shih-Han ; Li, Liyi ; Hicks, Michael

    Abstract | Document (853 KB) | BibTeX

    Formalization of Basic Combinatorics on Words
    Authors: Holub, Štěpán ; Starosta, Štěpán

    Abstract | Document (1,051 KB) | BibTeX

    Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq
    Authors: Kirst, Dominik ; Hermes, Marc

    Abstract | Document (783 KB) | BibTeX

    Complete Bidirectional Typing for the Calculus of Inductive Constructions
    Authors: Lennon-Bertrand, Meven

    Abstract | Document (833 KB) | BibTeX

    A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks
    Authors: Lochbihler, Andreas

    Abstract | Document (873 KB) | BibTeX

    A Formal Proof of Modal Completeness for Provability Logic
    Authors: Maggesi, Marco ; Perini Brogi, Cosimo

    Abstract | Document (716 KB) | BibTeX

    Formal Verification of Termination Criteria for First-Order Recursive Functions
    Authors: Muñoz, Cesar A. ; Ayala-Rincón, Mauricio ; Moscato, Mariano M. ; Dutle, Aaron M. ; Narkawicz, Anthony J. ; Almeida, Ariane A. ; Avelar, Andréia B. ; M. Ferreira Ramos, Thiago

    Abstract | Document (879 KB) | BibTeX

    Verified Double Sided Auctions for Financial Markets
    Authors: Natarajan, Raja ; Sarswat, Suneel ; Singh, Abhishek Kr

    Abstract | Document (717 KB) | BibTeX

    Reaching for the Star: Tale of a Monad in Coq
    Authors: Nigron, Pierre ; Dagand, Pierre-Évariste

    Abstract | Document (739 KB) | BibTeX

    Specifying Message Formats with Contiguity Types
    Authors: Slind, Konrad

    Abstract | Document (644 KB) | BibTeX

    Proof Pearl : Playing with the Tower of Hanoi Formally
    Authors: Théry, Laurent

    Abstract | Document (649 KB) | BibTeX

    Verifying an HTTP Key-Value Server with Interaction Trees and VST
    Authors: Zhang, Hengchu ; Honoré, Wolf ; Koh, Nicolas ; Li, Yao ; Li, Yishuai ; Xia, Li-Yao ; Beringer, Lennart ; Mansky, William ; Pierce, Benjamin ; Zdancewic, Steve

    Abstract | Document (752 KB) | BibTeX

    		  



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