Interactive Theorem Proving 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings /
This book constitutes the refereed proceedings of the 8th International Conference on Interactive Theorem Proving, ITP 2017, held in Brasilia, Brazil, in September 2017. The 28 full papers, 2 rough diamond papers, and 3 invited talk papers presented were carefully reviewed and selected from 65 submi...
| Corporate Author: | |
|---|---|
| Other Authors: | , |
| Language: | English |
| Published: |
Cham :
Springer International Publishing : Imprint: Springer,
2017.
|
| Edition: | 1st ed. 2017. |
| Series: | Theoretical Computer Science and General Issues ;
10499 |
| Subjects: | |
| Online Access: | https://doi.org/10.1007/978-3-319-66107-0 |
Table of Contents:
- 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.