Interactive Theorem Proving

Interactive Theorem Proving

6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings
Christian Urban, Xingyuan Zhang (eds.)

Table of Contents
Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems - pages 1-16 Abdulaziz, Mohammad (et al.)
Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory - pages 17-33 Affeldt, Reynald (et al.)
ROSCoq: Robots Powered by Constructive Reals - pages 34-50 Anand, Abhishek (et al.)
Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface - pages 51-66 Barras, Bruno (et al.)
A Concrete Memory Model for CompCert - pages 67-83 Besson, Frédéric (et al.)
Validating Dominator Trees for a Fast, Verified Dominance Test - pages 84-99 Blazy, Sandrine (et al.)
Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra - pages 100-116 Boulmé, Sylvain (et al.)
Mechanisation of AKS Algorithm: Part 1 – The Main Theorem - pages 117-136 Chan, Hing-Lun (et al.)
Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation - pages 137-153 Charguéraud, Arthur (et al.)
Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker - pages 154-169 Cruz-Filipe, Luís (et al.)
Proof-Producing Reflection for HOL - pages 170-186 Fallenstein, Benja (et al.)
Improved Tool Support for Machine-Code Decompilation in HOL4 - pages 187-202 Fox, Anthony
A Formalized Hierarchy of Probabilistic System Types - pages 203-220 Hölzl, Johannes (et al.)
A Verified Enclosure for the Lorenz Attractor (Rough Diamond) - pages 221-226 Immler, Fabian
Learning to Parse on Aligned Corpora (Rough Diamond) - pages 227-233 Kaliszyk, Cezary (et al.)
A Consistent Foundation for Isabelle/HOL - pages 234-252 Kuncar, Ondrej (et al.)
Refinement to Imperative/HOL - pages 253-269 Lammich, Peter
Stream Fusion for Isabelle’s Code Generator - pages 270-277 Lochbihler, Andreas (et al.)
HOCore in Coq - pages 278-293 Maksimovic, Petar (et al.)
Affine Arithmetic and Applications to Real-Number Proving - pages 294-309 Moscato, Mariano M. (et al.)
Amortized Complexity Verified - pages 310-324 Nipkow, Tobias
Foundational Property-Based Testing - pages 325-343 Paraskevopoulou, Zoe (et al.)
A Linear First-Order Functional Intermediate Language for Verified Compilers - pages 344-358 Schneider, Sigurd (et al.)
Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions - pages 359-374 Schäfer, Steven (et al.)
ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages - pages 375-390 Sieczkowski, Filip (et al.)
Transfinite Constructions in Classical Type Theory - pages 391-404 Smolka, Gert (et al.)
A Mechanized Theory of Regular Trees in Dependent Type Theory - pages 405-420 Spadotti, Régis
Deriving Comparators and Show Functions in Isabelle/HOL - pages 421-437 Sternagel, Christian (et al.)
Formalising Knot Theory in Isabelle/HOL - pages 438-452 Prathamesh, T. V. H.
Pattern Matches in HOL: A new Representation improved Code Generation - pages 453-468 Tuerk, Thomas (et al.)


Lecture Notes in Computer Science - Volume 9236


Springer, Paperback, english, 468 pages