Cover image for Interactive Theorem Proving 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings
Title:
Interactive Theorem Proving 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings
Author:
Urban, Christian. editor.
ISBN:
9783319221021
Edition:
1st ed. 2015.
Physical Description:
XI, 469 p. 63 illus. online resource.
Series:
Theoretical Computer Science and General Issues, 9236
Contents:
Verified, Practical Upper Bounds for State Space Diameters -- Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory -- ROSCoq: Robots powered by Constructive Reals -- Asynchronous processing of Coq documents: from the kernel up to the user interface -- A Concrete Memory Model for CompCert -- Validating Dominator Trees for a Fast, Verified Dominance Test -- Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra -- Mechanisation of AKS Algorithm -- Machine-Checked Verification of the Correctness and Amortized -- Improved Tool Support for Machine-Code Decompilation in HOL4 -- A Formalized Hierarchy of Probabilistic System Types -- Learning To Parse on Aligned Corpora -- A Consistent Foundation for Isabelle/HOL -- Foundational Property-Based Testing -- A First-Order Functional Intermediate Language for Verified Compilers -- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions -- ModuRes: a Coq Library for Modular Reasoning about Concurrent -- Higher-Order Imperative Programming Languages -- Transfinite Constructions in Classical Type Theory -- A Mechanized Theory of regular trees in dependent type theory -- Deriving Comparators and Show-Functions in Isabelle/HOL -- Formalizing Knot Theory in Isabelle/HOL -- Pattern Matches in HOL: A New Representation and Improved Code Generation.
Added Corporate Author:
Holds:
Copies:

Available:*

Library
Material Type
Item Barcode
Shelf Number
Status
Item Holds
Searching...
E-Book 519043-1001 XX(519043.1)
Searching...

On Order