000 | 03601nam a22005655i 4500 | ||
---|---|---|---|
001 | 978-3-540-49562-8 | ||
003 | DE-He213 | ||
005 | 20160624102044.0 | ||
007 | cr nn 008mamaa | ||
008 | 121227s1998 gw | s |||| 0|eng d | ||
020 |
_a9783540495628 _9978-3-540-49562-8 |
||
024 | 7 |
_a10.1007/BFb0097782 _2doi |
|
050 | 4 | _aQA76.9.L63 | |
050 | 4 | _aQA76.5913 | |
050 | 4 | _aQA76.63 | |
072 | 7 |
_aUM _2bicssc |
|
072 | 7 |
_aUYF _2bicssc |
|
072 | 7 |
_aCOM051000 _2bisacsh |
|
072 | 7 |
_aCOM036000 _2bisacsh |
|
082 | 0 | 4 |
_a005.1015113 _223 |
245 | 1 | 0 |
_aTypes for Proofs and Programs _h[electronic resource] : _bInternational Workshop TYPES’96 Aussois, France, December 15–19, 1996 Selected Papers / _cedited by Eduardo Giménez, Christine Paulin-Mohring. |
260 | 1 |
_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg, _c1998. |
|
264 | 1 |
_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg, _c1998. |
|
300 |
_aVIII, 380 p. _bonline resource. |
||
336 |
_atext _btxt _2rdacontent |
||
337 |
_acomputer _bc _2rdamedia |
||
338 |
_aonline resource _bcr _2rdacarrier |
||
347 |
_atext file _bPDF _2rda |
||
490 | 1 |
_aLecture Notes in Computer Science, _x0302-9743 ; _v1512 |
|
505 | 0 | _aCoercion 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 | _aThis 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 | _aComputer science. | |
650 | 0 | _aLogic design. | |
650 | 0 | _aArtificial intelligence. | |
650 | 1 | 4 | _aComputer Science. |
650 | 2 | 4 | _aLogics and Meanings of Programs. |
650 | 2 | 4 | _aMathematical Logic and Formal Languages. |
650 | 2 | 4 | _aProgramming Languages, Compilers, Interpreters. |
650 | 2 | 4 | _aArtificial Intelligence (incl. Robotics). |
700 | 1 |
_aGiménez, Eduardo. _eeditor. |
|
700 | 1 |
_aPaulin-Mohring, Christine. _eeditor. |
|
710 | 2 | _aSpringerLink (Online service) | |
773 | 0 | _tSpringer eBooks | |
776 | 0 | 8 |
_iPrinted edition: _z9783540651376 |
786 | _dSpringer | ||
830 | 0 |
_aLecture Notes in Computer Science, _x0302-9743 ; _v1512 |
|
856 | 4 | 0 | _uhttp://dx.doi.org/10.1007/BFb0097782 |
942 |
_2EBK6815 _cEBK |
||
999 |
_c36109 _d36109 |