Interactive Theorem Proving: 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings

Front Matter ....Pages I-XIX
 Automated Theory Exploration for Interactive Theorem Proving:  (Moa Johansson)....Pages 1-11
 Automating Formalization by Statistical and Semantic Parsing of Mathematics  (Cezary Kaliszyk, Josef Urban, Jiří Vyskočil)....Pages 12-27
 A Formalization of Convex Polyhedra Based on the Simplex Method  (Xavier Allamigeon, Ricardo D. Katz)....Pages 28-45
 A Formal Proof of the Expressiveness of Deep Learning  (Alexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow)....Pages 46-64
 Formalization of the Lindemann-Weierstrass Theorem  (Sophie Bernard)....Pages 65-80
 CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics  (Frédéric Besson, Sandrine Blazy, Pierre Wilke)....Pages 81-97
 Formal Verification of a Floating-Point Expansion Renormalization Algorithm  (Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu)....Pages 98-113
 How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation  (David Butler, David Aspinall, Adrià Gascón)....Pages 114-130
 FoCaLiZe and Dedukti to the Rescue for Proof Interoperability  (Raphaël Cauderlier, Catherine Dubois)....Pages 131-147
 A Formal Proof in Coq of LaSalle’s Invariance Principle  (Cyril Cohen, Damien Rouhling)....Pages 148-163
 How to Get More Out of Your Oracles  (Luís Cruz-Filipe, Kim S. Larsen, Peter Schneider-Kamp)....Pages 164-170
 Certifying Standard and Stratified Datalog Inference Engines in SSReflect  (Véronique Benzaken, Évelyne Contejean, Stefania Dumbrava)....Pages 171-188
 Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq  (Yannick Forster, Gert Smolka)....Pages 189-206
 Bellerophon: Tactical Theorem Proving for Hybrid Systems  (Nathan Fulton, Stefan Mitsch, Brandon Bohrer, André Platzer)....Pages 207-224
 Formalizing Basic Quaternionic Analysis  (Andrea Gabrielli, Marco Maggesi)....Pages 225-240
 A Formalized General Theory of Syntax with Bindings  (Lorenzo Gheri, Andrei Popescu)....Pages 241-261
 Proof Certificates in PVS  (Frédéric Gilbert)....Pages 262-268
 Efficient, Verified Checking of Propositional Proofs  (Marijn Heule, Warren Hunt Jr., Matt Kaufmann, Nathan Wetzler)....Pages 269-284
 Proof Tactics for Assertions in Separation Logic  (Zhé Hóu, David Sanán, Alwen Tiu, Yang Liu)....Pages 285-303
 Categoricity Results for Second-Order ZF in Dependent Type Theory  (Dominik Kirst, Gert Smolka)....Pages 304-318
 Making PVS Accessible to Generic Services by Interpretation in a Universal Format  (Michael Kohlhase, Dennis Müller, Sam Owre, Florian Rabe)....Pages 319-335
 Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft Dynamics  (Yanni Kouskoulas, Daniel Genin, Aurora Schmidt, Jean-Baptiste Jeannin)....Pages 336-353
 Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms  (Laureano Lambán, Francisco J. Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina)....Pages 354-370
 Typing Total Recursive Functions in Coq  (Dominique Larchey-Wendling)....Pages 371-388
 Effect Polymorphism in Higher-Order Logic (Proof Pearl)  (Andreas Lochbihler)....Pages 389-409
 Schulze Voting as Evidence Carrying Computation  (Dirk Pattinson, Mukesh Tiwari)....Pages 410-426
 Verified Spilling and Translation Validation with Repair  (Julian Rosemann, Sigurd Schneider, Sebastian Hack)....Pages 427-443
 A Verified Generational Garbage Collector for CakeML  (Adam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola)....Pages 444-461
 A Formalisation of Consistent Consequence for Boolean Equation Systems  (Myrthe van Delft, Herman Geuvers, Tim A. C. Willemse)....Pages 462-478
 Homotopy Type Theory in Lean  (Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz)....Pages 479-495
 Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology  (Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan et al.)....Pages 496-513
 Formalization of the Fundamental Group in Untyped Set Theory Using Auto2  (Bohua Zhan)....Pages 514-530
Back Matter ....Pages 531-532