دانلود کتاب Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings

فهرست مطالب :

Front Matter....Pages I-XI
Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems....Pages 1-16
Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory....Pages 17-33
ROSCoq: Robots Powered by Constructive Reals....Pages 34-50
Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface....Pages 51-66
A Concrete Memory Model for CompCert....Pages 67-83
Validating Dominator Trees for a Fast, Verified Dominance Test....Pages 84-99
Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra....Pages 100-116
Mechanisation of AKS Algorithm: Part 1 – The Main Theorem....Pages 117-136
Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation....Pages 137-153
Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker....Pages 154-169
Proof-Producing Reflection for HOL....Pages 170-186
Improved Tool Support for Machine-Code Decompilation in HOL4....Pages 187-202
A Formalized Hierarchy of Probabilistic System Types....Pages 203-220
A Verified Enclosure for the Lorenz Attractor (Rough Diamond)....Pages 221-226
Learning to Parse on Aligned Corpora (Rough Diamond)....Pages 227-233
A Consistent Foundation for Isabelle/HOL....Pages 234-252
Refinement to Imperative/HOL....Pages 253-269
Stream Fusion for Isabelle’s Code Generator....Pages 270-277
HOCore in Coq....Pages 278-293
Affine Arithmetic and Applications to Real-Number Proving....Pages 294-309
Amortized Complexity Verified....Pages 310-324
Foundational Property-Based Testing....Pages 325-343
A Linear First-Order Functional Intermediate Language for Verified Compilers....Pages 344-358
Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions....Pages 359-374
ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages....Pages 375-390
Transfinite Constructions in Classical Type Theory....Pages 391-404
A Mechanized Theory of Regular Trees in Dependent Type Theory....Pages 405-420
Deriving Comparators and Show Functions in Isabelle/HOL....Pages 421-437
Formalising Knot Theory in Isabelle/HOL....Pages 438-452
Pattern Matches in HOL:....Pages 453-468
Back Matter....Pages 469-469