| 000 | 05678cam a22008294a 4500 | ||
|---|---|---|---|
| 001 | ocm50739382 | ||
| 003 | OCoLC | ||
| 005 | 20250703142916.0 | ||
| 006 | m o d | ||
| 007 | cr |n||||||||| | ||
| 008 | 020213s2002 gw a ob 101 0 eng c | ||
| 040 |
_aCOO _beng _epn _cCOO _dHNK _dOCLCQ _dYNG _dOCLCQ _dDKDLA _dOCLCQ _dGW5XE _dOCLCF _dOCLCQ _dOCLCO _dOCL _dOCLCO _dOCLCQ _dYDX _dDGU _dUAB _dESU _dOCLCQ _dVT2 _dBUF _dAU@ _dOCLCO _dWYU _dOCLCQ _dQE2 _dOCLCQ _dAUD _dOCLCQ _dHS0 _dUWK _dSXB _dOCLCQ _dEUX _dUKAHL _dOCLCO _dOCLCQ _dOCLCO _dOCLCL |
||
| 015 |
_aGBA220709 _2bnb |
||
| 016 | 7 |
_a963684981 _2DE-101 |
|
| 019 |
_a729901619 _a769773057 _a990473038 _a1005821132 _a1057973409 _a1066563159 _a1081280099 _a1084950992 _a1105590242 _a1114522439 _a1162786906 _a1164870509 _a1166085316 _a1173876222 _a1238250584 |
||
| 020 |
_a9783540458425 _q(electronic bk.) |
||
| 020 |
_a3540458425 _q(electronic bk.) |
||
| 020 | _z3540432876 | ||
| 020 | _z9783540432876 | ||
| 024 | 7 |
_a10.1007/3-540-45842-5. _2doi |
|
| 029 | 1 |
_aAU@ _b000051346818 |
|
| 029 | 1 |
_aAU@ _b000051686613 |
|
| 029 | 1 |
_aAU@ _b000058016384 |
|
| 029 | 1 |
_aNZ1 _b14994648 |
|
| 029 | 1 |
_aNZ1 _b15296031 |
|
| 029 | 1 |
_aAU@ _b000060386869 |
|
| 035 |
_a(OCoLC)50739382 _z(OCoLC)729901619 _z(OCoLC)769773057 _z(OCoLC)990473038 _z(OCoLC)1005821132 _z(OCoLC)1057973409 _z(OCoLC)1066563159 _z(OCoLC)1081280099 _z(OCoLC)1084950992 _z(OCoLC)1105590242 _z(OCoLC)1114522439 _z(OCoLC)1162786906 _z(OCoLC)1164870509 _z(OCoLC)1166085316 _z(OCoLC)1173876222 _z(OCoLC)1238250584 |
||
| 042 | _apcc | ||
| 050 | 4 |
_aQA76.9.A96 _bT96 2000 |
|
| 055 | 3 |
_aQA75 _b.L38 no.2277 |
|
| 072 | 7 |
_aQA _2lcco |
|
| 072 | 7 |
_aUM. _2bicssc |
|
| 072 | 7 |
_aUYF. _2bicssc |
|
| 072 | 7 |
_aCOM051000. _2bisacsh |
|
| 072 | 7 |
_aCOM036000. _2bisacsh |
|
| 082 | 0 | 4 |
_a006.3/33 _221 |
| 084 |
_a54.10 _2bcl |
||
| 084 |
_aSS 4800 _2rvk |
||
| 049 | _aMAIN | ||
| 111 | 2 |
_aTYPES 2000 _d(2000 : _cDurham, England) _917020 |
|
| 245 | 1 | 0 |
_aTypes for proofs and programs : _bInternational Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers / _cPaul Callaghan [and others]. |
| 260 |
_aBerlin ; _aNew York : _bSpringer, _c©2002. |
||
| 300 |
_a1 online resource (viii, 242 pages) : _billustrations |
||
| 336 |
_atext _btxt _2rdacontent |
||
| 337 |
_acomputer _bc _2rdamedia |
||
| 338 |
_aonline resource _bcr _2rdacarrier |
||
| 490 | 1 |
_aLecture notes in computer science ; _v2277 |
|
| 504 | _aIncludes bibliographical references and index. | ||
| 520 | _aThis book constitutes the thoroughly refereed post-proceedings of the International Workshop of the TYPES Working Group, TYPES 2000, held in Durham, UK in December 2000. The 15 revised full papers presented were carefully reviewed and selected during two rounds of refereeing and revision. All current issues on type theory and type systems and their applications to programming, systems design, and proof theory are addressed. | ||
| 505 | 0 | _aCollection Principles in Dependent Type Theory / Peter Aczel and Nicola Gambino -- Executing Higher Order Logic / Stefan Berghofer and Tobias Nipkow -- A Tour with Constructive Real Numbers / Alberto Ciaffaglione and Pietro Di Gianantonio -- An Implementation of Type:Type / Thierry Coquand and Makoto Takeyama -- On the Logical Content of Computational Type Theory: A Solution to Curry's Problem / Matt Fairtlough and Michael Mendler -- Constructive Reals in Coq: Axioms and Categoricity / Herman Geuvers and Milad Niqui -- A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals / Herman Geuvers, Freck Wiedijk and Jan Zwanenburg -- A Kripke-Style Model for the Admissibility of Structural Rules / Healfdene Goguen -- Towards Limit Computable Mathematics / Susumu Hayashi and Masahiro Nakata -- Formalizing the Halting Problem in a Constructive Type Theory / Kristofer Johannisson -- On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory / Giuseppe Longo -- Changing Data Structures in Type Theory: A Study of Natural Numbers / Nicolas Magaud and Yves Bertot -- Elimination with a Motive / Conor McBride -- Generalization in Type Theory Based Proof Assistants / Olivier Pons -- An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman's Lemma / Monika Seisenberger. | |
| 546 | _aEnglish. | ||
| 650 | 0 |
_aAutomatic theorem proving _vCongresses. _914919 |
|
| 650 | 0 |
_aComputer programming _vCongresses. |
|
| 650 | 6 |
_aThéorèmes _xDémonstration automatique _vCongrès. _914921 |
|
| 650 | 6 |
_aProgrammation (Informatique) _vCongrès. |
|
| 650 | 7 |
_aAutomatic theorem proving _2fast _914923 |
|
| 650 | 7 |
_aComputer programming _2fast _93021 |
|
| 653 |
_aFACinfotech _aComputer science |
||
| 653 |
_aER _aInternet _aBook _aFull text |
||
| 655 | 7 |
_aproceedings (reports) _2aat |
|
| 655 | 7 |
_aConference papers and proceedings _2fast _96065 |
|
| 655 | 7 |
_aConference papers and proceedings. _2lcgft _96065 |
|
| 655 | 7 |
_aActes de congrès. _2rvmgf _9609890 |
|
| 700 | 1 |
_aCallaghan, Paul, _d1970- _1https://id.oclc.org/worldcat/entity/E39PCjGB7JGwMCcQrmqjCMC8Fq _917022 |
|
| 758 |
_ihas work: _aTypes for proofs and programs (Text) _1https://id.oclc.org/worldcat/entity/E39PCGyWFGrMjvHB3KJggB3TXm _4https://id.oclc.org/worldcat/ontology/hasWork |
||
| 776 | 0 | 8 |
_iPrint version:TYPES 2000 (2000 : Durham, England) _tTypes for proofs and programs : International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000 : selected papers. _w(OCoLC)49197579 |
| 830 | 0 |
_aLecture notes in computer science ; _v2277. |
|
| 856 | 4 | 0 | _uhttps://link.springer.com/10.1007/3-540-45842-5 |
| 938 |
_aAskews and Holts Library Services _bASKH _nAH26902049 |
||
| 938 |
_aYBP Library Services _bYANK _n13351101 |
||
| 994 |
_a92 _bATIST |
||
| 999 |
_c635539 _d635539 |
||