000			02889nam a22003615i 4500
001			321511
003			MX-SnUAN
005			20160429161505.0
007			cr nn 008mamaa
008			160111s2015 gw | s |||| 0|eng d
020			_a9783319221021 _9978-3-319-22102-1
035			_avtls000422093
039		9	_y201601111020 _zstaff
050		4	_aQA8.9-QA10.3
245	1	0	_aInteractive theorem proving : _b6th international conference, itp 2015, nanjing, china, august 24-27, 2015, proceedings / _cedited by Christian Urban, Xingyuan Zhang.
250			_a1st ed. 2015.
264		1	_aCham : _bSpringer International Publishing : _bSpringer, _c2015.
300			_axi, 469 páginas : _b63 ilustraciones
336			_atexto _btxt _2rdacontent
337			_acomputadora _bc _2rdamedia
338			_arecurso en línea _bcr _2rdacarrier
347			_aarchivo de texto _bPDF _2rda
490	0		_aLecture Notes in Computer Science, _x0302-9743 ; _v9236
500			_aSpringer eBooks
505	0		_aVerified, 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.
590			_aPara consulta fuera de la UANL se requiere clave de acceso remoto.
700	1		_aUrban, Christian, _eeditor. _9337876
700	1		_aZhang, Xingyuan, _eeditor. _9366510
710	2		_aSpringerLink (Servicio en línea) _9299170
776	0	8	_iEdición impresa: _z9783319221014
856	4	0	_uhttp://remoto.dgb.uanl.mx/login?url=http://dx.doi.org/10.1007/978-3-319-22102-1 _zConectar a Springer E-Books (Para consulta externa se requiere previa autentificación en Biblioteca Digital UANL)
942			_c14
999			_c321511 _d321511