TY  - BOOK
AU  - Urban,Christian
AU  - Zhang,Xingyuan
TI  - Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings 
SN  - 9783319221021
PY  - 2015///
CY  - Cham
PB  - Springer International Publishing
KW  - Computer science
KW  - Software engineering
KW  - Computer security
KW  - Algorithms
KW  - Computer logic
KW  - Mathematical logic
KW  - Artificial intelligence
N1  - 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
UR  - http://dx.doi.org/10.1007/978-3-319-22102-1
ER  -