Interactive Theorem Proving

Front Matter ....Pages I-XVII
 Physical Addressing on Real Hardware in Isabelle/HOL  (Reto Achermann, Lukas Humbel, David Cock, Timothy Roscoe)....Pages 1-19
 Towards Certified Meta-Programming with Typed Template-Coq  (Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau)....Pages 20-39
 Formalizing Ring Theory in PVS  (Andréia B. Avelar da Silva, Thaynara Arielly de Lima, André Luiz Galdino)....Pages 40-47
 Software Tool Support for Modular Reasoning in Modal Logics of Actions  (Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano)....Pages 48-67
 Backwards and Forwards with Separation Logic  (Callum Bannister, Peter Höfner, Gerwin Klein)....Pages 68-87
 A Coq Formalisation of SQL’s Execution Engines  (V. Benzaken, É. Contejean, Ch. Keller, E. Martins)....Pages 88-107
 A Coq Tactic for Equality Learning in Linear Arithmetic  (Sylvain Boulmé, Alexandre Maréchal)....Pages 108-125
 The Coinductive Formulation of Common Knowledge  (Colm Baston, Venanzio Capretta)....Pages 126-141
 Tactics and Certificates in Meta Dedukti  (Raphaël Cauderlier)....Pages 142-159
 A Formalization of the LLL Basis Reduction Algorithm  (Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada)....Pages 160-177
 A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs  (Christian Doczkal, Guillaume Combette, Damien Pous)....Pages 178-195
 Verified Analysis of Random Binary Tree Structures  (Manuel Eberl, Max W. Haslbeck, Tobias Nipkow)....Pages 196-214
 HOL Light QE  (Jacques Carette, William M. Farmer, Patrick Laskowski)....Pages 215-234
 Efficient Mendler-Style Lambda-Encodings in Cedille  (Denis Firsov, Richard Blair, Aaron Stump)....Pages 235-252
 Verification of PCP-Related Computational Reductions in Coq  (Yannick Forster, Edith Heiter, Gert Smolka)....Pages 253-269
 ProofWatch: Watchlist Guidance for Large Theories in E  (Zarathustra Goertzel, Jan Jakubův, Stephan Schulz, Josef Urban)....Pages 270-288
 Reification by Parametricity  (Jason Gross, Andres Erbsen, Adam Chlipala)....Pages 289-305
 Verifying the LTL to Büchi Automata Translation via Very Weak Alternating Automata  (Simon Jantsch, Michael Norrish)....Pages 306-323
 CalcCheck: A Proof Checker for Teaching the “Logical Approach to Discrete Math”  (Wolfram Kahl)....Pages 324-341
 Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY  (Alexander Knüppel, Thomas Thüm, Carsten Immanuel Pardylla, Ina Schaefer)....Pages 342-361
 Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB  (Ramana Kumar, Eric Mullen, Zachary Tatlock, Magnus O. Myreen)....Pages 362-369
 Proof Pearl: Constructive Extraction of Cycle Finding Algorithms  (Dominique Larchey-Wendling)....Pages 370-387
 Fast Machine Words in Isabelle/HOL  (Andreas Lochbihler)....Pages 388-410
 Relational Parametricity and Quotient Preservation for Modular (Co)datatypes  (Andreas Lochbihler, Joshua Schneider)....Pages 411-431
 Towards Verified Handwritten Calculational Proofs  (Alexandra Mendes, João F. Ferreira)....Pages 432-440
 A Formally Verified Solver for Homogeneous Linear Diophantine Equations  (Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel)....Pages 441-458
 Formalizing Implicative Algebras in Coq  (Étienne Miquey)....Pages 459-476
 Boosting the Reuse of Formal Specifications  (Mariano M. Moscato, Carlos G. Lopez Pombo, César A. Muñoz, Marco A. Feliú)....Pages 477-494
 Towards Formal Foundations for Game Theory  (Julian Parsert, Cezary Kaliszyk)....Pages 495-503
 Verified Timing Transformations in Synchronous Circuits with \\(\\lambda \\pi \\) -Ware  (João Paulo Pizani Flor, Wouter Swierstra)....Pages 504-522
 A Formal Equational Theory for Call-By-Push-Value  (Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic)....Pages 523-541
 Program Verification in the Presence of Cached Address Translation  (Hira Taqdees Syeda, Gerwin Klein)....Pages 542-559
 Verified Tail Bounds for Randomized Programs  (Joseph Tassarotti, Robert Harper)....Pages 560-578
 Verified Memoization and Dynamic Programming  (Simon Wimmer, Shuwei Hu, Tobias Nipkow)....Pages 579-596
 MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)  (Simon Wimmer, Johannes Hölzl)....Pages 597-603
 Formalization of a Polymorphic Subtyping Algorithm  (Jinxu Zhao, Bruno C. d. S. Oliveira, Tom Schrijvers)....Pages 604-622
 An Agda Formalization of Üresin and Dubois’ Asynchronous Fixed-Point Theory  (Ran Zmigrod, Matthew L. Daggitt, Timothy G. Griffin)....Pages 623-639
Back Matter ....Pages 641-642