000			03783nam a22003495i 4500
001			318374
003			MX-SnUAN
005			20160429161130.0
007			cr nn 008mamaa
008			160108s2014 gw | s |||| 0|eng d
020			_a9783319089706 _9978-3-319-08970-6
035			_avtls000417930
039		9	_y201601081147 _zstaff
050		4	_aQA8.9-QA10.3
245	1	0	_aInteractive theorem proving : _b5th international conference, itp 2014, held as part of the vienna summer of logic, vsl 2014, vienna, austria, july 14-17, 2014. Proceedings / _cedited by Gerwin Klein, Ruben Gamboa.
264		1	_aCham : _bSpringer International Publishing : _bSpringer, _c2014.
300			_axxii, 555 páginas : _b90 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 ; _v8558
500			_aSpringer eBooks
505	0		_aMicrocode Verification – Another Piece of the Microprocessor Verification Puzzle -- Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK -- Towards a Formally Verified Proof Assistant -- Implicational Rewriting Tactics in HOL -- A Heuristic Prover for Real Inequalities -- A Formal Library for Elliptic Curves in the Coq Proof Assistant -- Truly Modular (Co) data types for Isabelle/HOL -- Cardinals in Isabelle/HOL -- Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code -- Showing Invariance Compositionally for a Process Algebra for Network Protocols -- A Computer-Algebra-Based Formal Proof of the Irrationality of ?(3) -- From Operational Models to Information Theory; Side Channels in pGCL with Isabelle -- A Coq Formalization of Finitely Presented Modules -- Formalized, Effective Domain Theory in Coq -- Completeness and Decidability Results for CTL in Coq -- Hypermap Specification and Certified Linked Implementation Using Orbits -- A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction -- Experience Implementing a Performant Category-Theory Library in Coq -- A New and Formalized Proof of Abstract Completion -- HOL with Definitions: Semantics, Soundness and a Verified Implementation -- Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm -- Recursive Functions on Lazy Lists via Domains and Topologies -- Formal Verification of Optical Quantum Flip Gate -- Compositional Computational Reflection -- An Isabelle Proof Method Language -- Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete -- The Reflective Milawa Theorem Prover Is Sound (Down to the Machine Code That Runs It) -- Balancing Lists: A Proof Pearl -- Unified Decision Procedures for Regular Expression Equivalence -- Collaborative Interactive Theorem Proving with Clide -- On the Formalization of Z-Transform in HOL -- Universe Polymorphism in Coq -- Asynchronous User Interaction and Tool Integration in Isabelle/PIDE -- HOL Constant Definition Done Right -- Rough Diamond: An Extension of Equivalence-Based Rewriting -- Formal C Semantics: Comp Cert and the C Standard -- Mechanical Certification of Loop Pipelining Transformations: A Preview.
590			_aPara consulta fuera de la UANL se requiere clave de acceso remoto.
700	1		_aKlein, Gerwin, _eeditor. _9362252
700	1		_aGamboa, Ruben, _eeditor. _9362253
710	2		_aSpringerLink (Servicio en línea) _9299170
776	0	8	_iEdición impresa: _z9783319089690
856	4	0	_uhttp://remoto.dgb.uanl.mx/login?url=http://dx.doi.org/10.1007/978-3-319-08970-6 _zConectar a Springer E-Books (Para consulta externa se requiere previa autentificación en Biblioteca Digital UANL)
942			_c14
999			_c318374 _d318374