Interactive theorem proving : (Registro nro. 318374)
[ vista simple ]
| 000 -CABECERA | |
|---|---|
| campo de control de longitud fija | 03783nam a22003495i 4500 |
| 001 - NÚMERO DE CONTROL | |
| campo de control | 318374 |
| 003 - IDENTIFICADOR DEL NÚMERO DE CONTROL | |
| campo de control | MX-SnUAN |
| 005 - FECHA Y HORA DE LA ÚLTIMA TRANSACCIÓN | |
| campo de control | 20160429161130.0 |
| 007 - CAMPO FIJO DE DESCRIPCIÓN FÍSICA--INFORMACIÓN GENERAL | |
| campo de control de longitud fija | cr nn 008mamaa |
| 008 - DATOS DE LONGITUD FIJA--INFORMACIÓN GENERAL | |
| campo de control de longitud fija | 160108s2014 gw | s |||| 0|eng d |
| 020 ## - NÚMERO INTERNACIONAL ESTÁNDAR DEL LIBRO | |
| Número Internacional Estándar del Libro | 9783319089706 |
| -- | 978-3-319-08970-6 |
| 035 ## - NÚMERO DE CONTROL DEL SISTEMA | |
| Número de control de sistema | vtls000417930 |
| 039 #9 - NIVEL DE CONTROL BIBLIOGRÁFICO Y DETALLES DE CODIFICACIÓN [OBSOLETO] | |
| -- | 201601081147 |
| -- | staff |
| 050 #4 - CLASIFICACIÓN DE LA BIBLIOTECA DEL CONGRESO | |
| Número de clasificación | QA8.9-QA10.3 |
| 245 10 - MENCIÓN DE TÍTULO | |
| Título | Interactive theorem proving : |
| Resto del título | 5th international conference, itp 2014, held as part of the vienna summer of logic, vsl 2014, vienna, austria, july 14-17, 2014. Proceedings / |
| Mención de responsabilidad, etc. | edited by Gerwin Klein, Ruben Gamboa. |
| 264 #1 - PRODUCCIÓN, PUBLICACIÓN, DISTRIBUCIÓN, FABRICACIÓN Y COPYRIGHT | |
| Producción, publicación, distribución, fabricación y copyright | Cham : |
| Nombre del de productor, editor, distribuidor, fabricante | Springer International Publishing : |
| -- | Springer, |
| Fecha de producción, publicación, distribución, fabricación o copyright | 2014. |
| 300 ## - DESCRIPCIÓN FÍSICA | |
| Extensión | xxii, 555 páginas : |
| Otras características físicas | 90 ilustraciones |
| 336 ## - TIPO DE CONTENIDO | |
| Término de tipo de contenido | texto |
| Código de tipo de contenido | txt |
| Fuente | rdacontent |
| 337 ## - TIPO DE MEDIO | |
| Nombre/término del tipo de medio | computadora |
| Código del tipo de medio | c |
| Fuente | rdamedia |
| 338 ## - TIPO DE SOPORTE | |
| Nombre/término del tipo de soporte | recurso en línea |
| Código del tipo de soporte | cr |
| Fuente | rdacarrier |
| 347 ## - CARACTERÍSTICAS DEL ARCHIVO DIGITAL | |
| Tipo de archivo | archivo de texto |
| Formato de codificación | |
| Fuente | rda |
| 490 0# - MENCIÓN DE SERIE | |
| Mención de serie | Lecture Notes in Computer Science, |
| Número Internacional Normalizado para Publicaciones Seriadas | 0302-9743 ; |
| Designación de volumen o secuencia | 8558 |
| 500 ## - NOTA GENERAL | |
| Nota general | Springer eBooks |
| 505 0# - NOTA DE CONTENIDO CON FORMATO | |
| Nota de contenido con formato | Microcode 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 ## - NOTA LOCAL (RLIN) | |
| Nota local | Para consulta fuera de la UANL se requiere clave de acceso remoto. |
| 700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA | |
| Nombre de persona | Klein, Gerwin, |
| Término indicativo de función/relación | editor. |
| 9 (RLIN) | 362252 |
| 700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA | |
| Nombre de persona | Gamboa, Ruben, |
| Término indicativo de función/relación | editor. |
| 9 (RLIN) | 362253 |
| 710 2# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE ENTIDAD CORPORATIVA | |
| Nombre de entidad corporativa o nombre de jurisdicción como elemento de entrada | SpringerLink (Servicio en línea) |
| 9 (RLIN) | 299170 |
| 776 08 - ENTRADA/ENLACE A UN FORMATO FÍSICO ADICIONAL | |
| Información de relación/Frase instructiva de referencia | Edición impresa: |
| Número Internacional Estándar del Libro | 9783319089690 |
| 856 40 - LOCALIZACIÓN Y ACCESO ELECTRÓNICOS | |
| Identificador Uniforme del Recurso | <a href="http://remoto.dgb.uanl.mx/login?url=http://dx.doi.org/10.1007/978-3-319-08970-6">http://remoto.dgb.uanl.mx/login?url=http://dx.doi.org/10.1007/978-3-319-08970-6</a> |
| Nota pública | Conectar a Springer E-Books (Para consulta externa se requiere previa autentificación en Biblioteca Digital UANL) |
| 942 ## - ELEMENTOS DE PUNTO DE ACCESO ADICIONAL (KOHA) | |
| Tipo de ítem Koha | Recurso en línea |
No hay ítems disponibles.