Interactive Theorem Proving: 8th International Conference, ITP 2017, Brasília, Brazil, September 26-
89.99 CHF
Versandkostenfrei
Lieferzeit: 7-14 Werktage
- Artikel-Nr.: 10461215
Beschreibung
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.
Eigenschaften
Breite: | 155 |
Gewicht: | 826 g |
Höhe: | 235 |
Länge: | 29 |
Seiten: | 532 |
Sprachen: | Englisch |
Autor: | César A. Muñoz, Mauricio Ayala-Rincón |
Bewertung
Bewertungen werden nach Überprüfung freigeschaltet.
Zuletzt angesehen