Tools

LEADER 02846cam a22004574a 4500

001 ocm45620936;

003 OCoLC;

005 20141212151939.0;

008 001218s2000 gw a b 101 0 eng ;

010 a| 00069849;

020 a| 3540415173 (softcover : alk. paper);

035 a| (Sirsi) o45620936;

035 a| (OCoLC)45620936;

042 a| pcc;

049 a| EREE;

050 00 a| QA76.9.A96b| T96 1999;

072 7 a| QA2| lcco;

082 00 a| 005.13/12| 21;

111 2 a| TYPES '99d| (1999 :c| Lökeberg, Sweden)=| ^A481527;

245 10 a| Types for proofs and programs :b| international workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers /c| Thierry Coquand [and others] (eds.).;

300 a| 193 pages :b| illustrations ;c| 24 cm.;

336 a| text2| rdacontent;

337 a| unmediated2| rdamedia;

338 a| volume2| rdacarrier;

490 1 a| Lecture notes in computer science ;v| 1956;

504 a| Includes bibliographical references and index.;

505 0 a| Specification and verification of a formal system for structurally recursive functions / Andreas Abel -- A predicative strong normalisation proof for a [lambda]-calculus with interleaving inductive types / Andreas Abel and Thorsten Altenkirch -- Polymorphic intersection type assignment for rewrite systems with abstraction and β-rule / Steffen van Bakel, Franco Barbanera, and Maribel Fernández -- Computer-assisted mathematics at work (the Hahn-Banach theorem in Isabelle/Isar) / Gertrud Bauer and Markus Wenzel -- Specification of a smart card operating system / Gustavo Betarte ... [et al.] -- Implementation techniques for inductive types in plastic / Paul Callaghan and Zhaohui Luo -- A co-inductive approach to real numbers / Alberto Ciaffaglione and Pietro Di Gianantonio -- Information retrieval in a Coq proof library using type isomorphisms / David Delahaye -- Memory management : an abstract formulation of incremental tracing / Healfdene Goguen, Richard Brooksby, and Rod Burstall -- The three gap theorem (Steinhaus conjecture) / Micaela Mayero -- Formalising formulas-as-types-as-objects / Qiao Haiyan.;

650 0 a| Automatic theorem provingv| Congresses.=| ^A24746;

650 0 a| Computer programmingv| Congresses.=| ^A34403;

650 0 a| Type theoryv| Congresses.=| ^A32232;

700 1 a| Coquand, Thierry,d| 1961-=| ^A481528;

830 0 a| Lecture notes in computer sciencev| 1956.=| ^A466336;

994 a| X0b| ERE;

910 a| PromptCat;

938 a| Otto Harrassowitzb| HARRn| har015000956c| 66.00 DEM;

980 a| 2001-05-30b| 45d| 2.57e| 42.75f| 837942;

596 a| 1;

998 a| 810818;

999 a| QA76.9.A96 T96 1999w| LCc| 1i| 30372010927652d| 3/6/2013f| 3/6/2013g| 1l| JGESm| JOYNERp| $42.75r| Ys| Yt| JGESBKu| 6/15/2001x| BOOKz| JSTACKSo| .STAFF. 0;

Types for proofs and programs : international workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers / Thierry Coquand [and others] (eds.).

Author/creator	TYPES '99
Other author	Coquand, Thierry, 1961-
Format	Book
Publication Info	Berlin ; New York : Springer, ©2000.
Description	193 pages : illustrations ; 24 cm.
Subjects	Automatic theorem proving--Congresses. Computer programming--Congresses. Type theory--Congresses.

Series	Lecture notes in computer science ; 1956 Lecture notes in computer science 1956. ^A466336
Contents	Specification and verification of a formal system for structurally recursive functions / Andreas Abel -- A predicative strong normalisation proof for a [lambda]-calculus with interleaving inductive types / Andreas Abel and Thorsten Altenkirch -- Polymorphic intersection type assignment for rewrite systems with abstraction and β-rule / Steffen van Bakel, Franco Barbanera, and Maribel Fernández -- Computer-assisted mathematics at work (the Hahn-Banach theorem in Isabelle/Isar) / Gertrud Bauer and Markus Wenzel -- Specification of a smart card operating system / Gustavo Betarte ... [et al.] -- Implementation techniques for inductive types in plastic / Paul Callaghan and Zhaohui Luo -- A co-inductive approach to real numbers / Alberto Ciaffaglione and Pietro Di Gianantonio -- Information retrieval in a Coq proof library using type isomorphisms / David Delahaye -- Memory management : an abstract formulation of incremental tracing / Healfdene Goguen, Richard Brooksby, and Rod Burstall -- The three gap theorem (Steinhaus conjecture) / Micaela Mayero -- Formalising formulas-as-types-as-objects / Qiao Haiyan.
Bibliography note	Includes bibliographical references and index.
LCCN	00069849
ISBN	3540415173 (softcover : alk. paper)

Availability

Library	Location	Call Number	Status	Item Actions
Joyner	General Stacks	QA76.9.A96 T96 1999	✔ Available	Place Hold

Types for proofs and programs : international workshop, TYPES '99, Lökeberg, Sweden, June 12-16, 1999 : selected papers / Thierry Coquand [and others] (eds.).

Click here for more information about this title

Availability