Interactive theorem proving : 6th international conference, itp 2015, nanjing, china, august 24-27, 2015, proceedings / edited by Christian Urban, Xingyuan Zhang.
Tipo de material:
TextoSeries Lecture Notes in Computer Science ; 9236Editor: Cham : Springer International Publishing : Springer, 2015Edición: 1st ed. 2015Descripción: xi, 469 páginas : 63 ilustracionesTipo de contenido: - texto
- computadora
- recurso en línea
- 9783319221021
- QA8.9-QA10.3
Springer eBooks
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.
Para consulta fuera de la UANL se requiere clave de acceso remoto.