E-grāmata: Interactive Theorem Proving: 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017, Proceedings

Whitebox Automation.- Automated Theory Exploration for Interactive Theorem Proving: An Introduction to the Hipster System.- Automating Formalization by Statistical and Semantic Parsing of Mathematics.- A Formalization of Convex Polyhedra Based on the Simplex Method.- A Formal Proof of the Expressiveness of Deep Learning.- Formalization of the Lindemann-Weierstrass Theorem.- CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics.- Formal Verification of a Floating-Point Expansion Renormalization Algorithm.- How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation.- FoCaLiZe and Dedukti to the Rescue for Proof Interoperability.- A Formal Proof in Coq of LaSalle's Invariance Principle.- How to Get More out of Your Oracles.- Certifying Standard and Stratified Datalog Inference Engines in SSReect.- Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq.- Bellerophon: Tactical Theorem Proving for Hybrid Systems.- Formalizing Basic Quaternionic Analysis.- A Formalized General Theory of Syntax with Bindings.- Proof Certificates in PVS.- Efficient, Verified Checking of Propositional Proofs.- Proof Tactics for Assertions in Separation Logic.- Categoricity Results for Second-Order ZF in Dependent Type Theory.- Making PVS Accessible to Generic Services by Interpretation in a Universal Format.- Formally Verified Safe Vertical Maneuvers for Non-Deterministic, Accelerating Aircraft Dynamics.- Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms.- Typing Total Recursive Functions in Coq.- Effect Polymorphism in Higher-Order Logic (Proof Pearl).- Schulze Voting as Evidence Carrying Computation.- Verified Spilling and Translation Validation with Repair.- A Verified Generational Garbage Collector for CakeML.- A Formalisation of Consistent Consequence for Boolean Equation Systems.- Homotopy Type Theory in Lean.- Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology.- Formalization of the Fundamental Group in Untyped Set Theory Using auto2.