Interactive theorem proving : 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings /: 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings. (2017)

• Record Type: Book
• Other Titles: ITP 2017
• Further Information: Note: Mauricio Ayala-Rincón, César A. Muñoz (eds.).
• Editors: Ayala-Rincón, M (Mauricio); Muñoz, César A, 1968-
• Other Names: ITP (Conference), 8th
• 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.
• Publisher Details: Cham, Switzerland : Springer
• Publication Date: 2017
• Extent: 1 online resource (xix, 532 pages), illustrations
• Subjects: 511.3/6028563; Computer science; Automatic theorem proving -- Congresses; Software engineering -- Congresses; Automatic theorem proving; Software engineering; Computers -- Programming -- General; Computers -- Hardware -- Handheld Devices; Computers -- Software Development & Engineering -- General; Computers -- Programming Languages -- General; Computers -- Intelligence (AI) & Semantics; Computer programming / software development; Systems analysis & design; Software Engineering; Programming & scripting languages: general; Artificial intelligence; Logic design; Computer system performance; Software engineering; Artificial intelligence; Mathematics -- Logic; Mathematical theory of computation; Electronic books; Conference papers and proceedings
• Languages: English
• ISBNs: 9783319661070; 3319661078
• Related ISBNs: 9783319661063; 331966106X
• Notes: Note: Online resource; title from PDF title page (SpringerLink, viewed September 8, 2017).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.