Interactive Theorem Proving : 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings /
| Autor Corporativo: | |
|---|---|
| Otros Autores: | , |
| Formato: | eBook |
| Lenguaje: | English |
| Publicado: |
Cham :
Springer International Publishing : Imprint: Springer,
2017.
|
| Edición: | 1st ed. 2017. |
| Colección: | Theoretical Computer Science and General Issues ;
10499 |
| Materias: |
Tabla de Contenidos:
- 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.