Types for Proofs and Programs (Record no. 36109)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 03601nam a22005655i 4500 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| ISBN | 9783540495628 |
| -- | 978-3-540-49562-8 |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER | |
| Classification number | 005.1015113 |
| 245 10 - TITLE STATEMENT | |
| Title | Types for Proofs and Programs |
| Sub Title | International Workshop TYPES’96 Aussois, France, December 15–19, 1996 Selected Papers / |
| Statement of responsibility, etc | edited by Eduardo Giménez, Christine Paulin-Mohring. |
| 260 #1 - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) | |
| Place of publication | Berlin, Heidelberg : |
| Name of publisher | Springer Berlin Heidelberg, |
| Year of publication | 1998. |
| 300 ## - PHYSICAL DESCRIPTION | |
| Number of Pages | VIII, 380 p. |
| Other physical details | online resource. |
| 490 1# - SERIES STATEMENT | |
| Series statement | Lecture Notes in Computer Science, |
| 505 0# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | Coercion synthesis in computer implementations of type-theoretic frameworks -- Verification of the interface of a small proof system in coq -- An implementation of the Heine-Borel covering theorem in type theory -- Detecting and removing dead-code using rank 2 intersection -- A type-free formalization of mathematics where proofs are objects -- Higman's lemma in type theory -- A proof of weak termination of typed ??-calculi -- Proof style -- Some algorithmic and proof-theoretical aspects of coercive subtyping -- Semantical BNF -- The internal type theory of a Heyting pretopos -- Inverting inductively defined relations in LEGO -- A generic normalisation proof for pure type systems -- Proving a real time algorithm for ATM in Coq -- Dependent types with explicit substitutions: A meta-theoretical development -- Type inference verified: Algorithm W in Isabelle/HOL -- Continuous lattices in formal topology -- Abstract insertion sort in an extension of type theory with record types and subtyping. |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc | This book constitutes the thoroughly revised post-workshop proceedings of the first annual workshop held under the auspices of the ESPRIT Working Group 21900 TYPES in Aussois, France in December 1996. The 18 revised full papers presented in the book were carefully reviewed and selected from the 30 papers accepted for presentation at the workshop. All current aspects of type theory and type systems and their applications to program verification and theorem proving are addressed; the proof systems and theorem provers dealt with include Coq, LEGO, and Isabelle/HOL. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical Term | Computer science. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical Term | Logic design. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical Term | Artificial intelligence. |
| 650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical Term | Computer Science. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical Term | Logics and Meanings of Programs. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical Term | Mathematical Logic and Formal Languages. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical Term | Programming Languages, Compilers, Interpreters. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical Term | Artificial Intelligence (incl. Robotics). |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Giménez, Eduardo. |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Paulin-Mohring, Christine. |
| 856 40 - ELECTRONIC LOCATION AND ACCESS | |
| Uniform Resource Identifier | http://dx.doi.org/10.1007/BFb0097782 |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) | |
| Koha item type | E-BOOKS |
| 264 #1 - | |
| -- | Berlin, Heidelberg : |
| -- | Springer Berlin Heidelberg, |
| -- | 1998. |
| 336 ## - | |
| -- | text |
| -- | txt |
| -- | rdacontent |
| 337 ## - | |
| -- | computer |
| -- | c |
| -- | rdamedia |
| 338 ## - | |
| -- | online resource |
| -- | cr |
| -- | rdacarrier |
| 347 ## - | |
| -- | text file |
| -- | |
| -- | rda |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE | |
| -- | 0302-9743 ; |
| Withdrawn status | Lost status | Damaged status | Not for loan | Current library | Accession Number | Uniform Resource Identifier | Koha item type |
|---|---|---|---|---|---|---|---|
| IMSc Library | EBK6815 | http://dx.doi.org/10.1007/BFb0097782 | E-BOOKS |