LIPIcs, Volume 193, ITP 2021

• Liron Cohen and Cezary Kaliszyk LIPIcs, Volume 193, ITP 2021, Complete Volume 10.4230/LIPIcs.ITP.2021
• Liron Cohen and Cezary Kaliszyk Front Matter, Table of Contents, Preface, Conference Organization 10.4230/LIPIcs.ITP.2021.0
• Magnus O. Myreen The CakeML Project’s Quest for Ever Stronger Correctness Theorems (Invited Paper) 10.4230/LIPIcs.ITP.2021.1
• Nadia Polikarpova Synthesis of Safe Pointer-Manipulating Programs (Invited Talk) 10.4230/LIPIcs.ITP.2021.2
• Andrei Popescu, Thomas Bauereiss, and Peter Lammich Bounded-Deducibility Security (Invited Paper) 10.4230/LIPIcs.ITP.2021.3
• Edward W. Ayers, Mateja Jamnik, and W. T. Gowers A Graphical User Interface Framework for Formal Verification 10.4230/LIPIcs.ITP.2021.4
• Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio A Formalization of Dedekind Domains and Class Groups of Global Fields 10.4230/LIPIcs.ITP.2021.5
• Seulkee Baek A Formally Verified Checker for First-Order Proofs 10.4230/LIPIcs.ITP.2021.6
• Christoph Benzmüller and David Fuenmayor Value-Oriented Legal Argumentation in Isabelle/HOL 10.4230/LIPIcs.ITP.2021.7
• Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub Unsolvability of the Quintic Formalized in Dependent Type Theory 10.4230/LIPIcs.ITP.2021.8
• Frédéric Besson Itauto: An Extensible Intuitionistic SAT Solver 10.4230/LIPIcs.ITP.2021.9
• Matthias Brun, Sára Decova, Andrea Lattuada, and Dmitriy Traytel Verified Progress Tracking for Timely Dataflow 10.4230/LIPIcs.ITP.2021.10
• Czesław Byliński, Artur Korniłowicz, and Adam Naumowicz Syntactic-Semantic Form of Mizar Articles 10.4230/LIPIcs.ITP.2021.11
• Joshua Chen Homotopy Type Theory in Isabelle 10.4230/LIPIcs.ITP.2021.12
• Luca Ciccone, Francesco Dagnino, and Elena Zucca Flexible Coinduction in Agda 10.4230/LIPIcs.ITP.2021.13
• Katherine Cordwell, Yong Kiam Tan, and André Platzer A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm 10.4230/LIPIcs.ITP.2021.14
• Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti Formalising a Turing-Complete Choreographic Language in Coq 10.4230/LIPIcs.ITP.2021.15
• Adrian De Lon, Peter Koepke, and Anton Lorenzen A Natural Formalization of the Mutilated Checkerboard Problem in Naproche 10.4230/LIPIcs.ITP.2021.16
• Christian Doczkal A Variant of Wagner’s Theorem Based on Combinatorial Hypermaps 10.4230/LIPIcs.ITP.2021.17
• Floris van Doorn Formalized Haar Measure 10.4230/LIPIcs.ITP.2021.18
• Yannick Forster, Fabian Kunze, Gert Smolka, and Maximilian Wuttke A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus 10.4230/LIPIcs.ITP.2021.19
• Lennard Gäher and Fabian Kunze Mechanising Complexity Theory: The Cook-Levin Theorem in Coq 10.4230/LIPIcs.ITP.2021.20
• Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks Proving Quantum Programs Correct 10.4230/LIPIcs.ITP.2021.21
• Štěpán Holub and Štěpán Starosta Formalization of Basic Combinatorics on Words 10.4230/LIPIcs.ITP.2021.22
• Dominik Kirst and Marc Hermes Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq 10.4230/LIPIcs.ITP.2021.23
• Meven Lennon-Bertrand Complete Bidirectional Typing for the Calculus of Inductive Constructions 10.4230/LIPIcs.ITP.2021.24
• Andreas Lochbihler A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks 10.4230/LIPIcs.ITP.2021.25
• Marco Maggesi and Cosimo Perini Brogi A Formal Proof of Modal Completeness for Provability Logic 10.4230/LIPIcs.ITP.2021.26
• Cesar A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron M. Dutle, Anthony J. Narkawicz, Ariane A. Almeida, Andréia B. Avelar, and Thiago M. Ferreira Ramos Formal Verification of Termination Criteria for First-Order Recursive Functions 10.4230/LIPIcs.ITP.2021.27
• Raja Natarajan, Suneel Sarswat, and Abhishek Kr Singh Verified Double Sided Auctions for Financial Markets 10.4230/LIPIcs.ITP.2021.28
• Pierre Nigron and Pierre-Évariste Dagand Reaching for the Star: Tale of a Monad in Coq 10.4230/LIPIcs.ITP.2021.29
• Konrad Slind Specifying Message Formats with Contiguity Types 10.4230/LIPIcs.ITP.2021.30
• Laurent Théry Proof Pearl : Playing with the Tower of Hanoi Formally 10.4230/LIPIcs.ITP.2021.31
• Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic Verifying an HTTP Key-Value Server with Interaction Trees and VST 10.4230/LIPIcs.ITP.2021.32