Normal view MARC view ISBD view

Types for proofs and programs : (Record no. 639297)

MARC details
000 -LEADER
fixed length control field	06566cam a2201057 a 4500
001 - CONTROL NUMBER
control field	ocn432712655
003 - CONTROL NUMBER IDENTIFIER
control field	OCoLC
005 - DATE AND TIME OF LATEST TRANSACTION
control field	20250703150701.0
006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS
fixed length control field	m o d
007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION
fixed length control field	cr cn\|\|\|\|\|\|\|\|\|
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field	090824s2009 gw a ob 101 0 eng d
040 ## - CATALOGING SOURCE
Original cataloging agency	GW5XE
Language of cataloging	eng
Description conventions	pn
Transcribing agency	GW5XE
Modifying agency	OCLCQ
--	MND
--	WAU
--	OSU
--	HNK
--	E7B
--	OCLCQ
--	OCLCO
--	OCLCQ
--	OCLCF
--	BEDGE
--	OCLCQ
--	OCLCO
--	A7U
--	YDXCP
--	IDEBK
--	NUI
--	OCL
--	OCLCO
--	EBLCP
--	OCLCQ
--	VT2
--	OCLCQ
--	ESU
--	OCLCQ
--	SHS
--	CEF
--	U3W
--	WYU
--	LHU
--	OCLCO
--	YOU
--	CNTRU
--	OCLCQ
--	AUD
--	OCLCQ
--	OCLCA
--	LUN
--	DCT
--	OCLCO
--	COM
--	OCLCO
--	SFB
--	QGK
--	OCLCQ
--	INT
--	OCLCO
--	OCLCL
--	OCLCQ
--	OCLCA
015 ## - NATIONAL BIBLIOGRAPHY NUMBER
National bibliography number	09,N27,0040
Source	dnb
016 7# - NATIONAL BIBLIOGRAPHIC AGENCY CONTROL NUMBER
Record control number	994783744
Source	DE-101
019 ## -
--	428884845
--	432209626
--	488556420
--	613528865
--	647818564
--	880316574
--	964932863
--	1005835888
--	1044245650
--	1056378025
--	1073061940
--	1081244279
--	1097279373
--	1100827105
--	1105596902
--	1171539394
--	1171846439
--	1203991694
--	1259224522
--	1262684316
--	1374612617
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number	9783642024443
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number	3642024440
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number	3642024432
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number	9783642024436
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number	9788364202445
Qualifying information	(3)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number	8364202448
024 7# - OTHER STANDARD IDENTIFIER
Standard number or code	10.1007/978-3-642-02444-3
Source of number or code	doi
028 00 - PUBLISHER NUMBER
Publisher number	Best.-Nr. 12697175
029 1# - (OCLC)
OCLC library identifier	AU@
System control number	000045250826
029 1# - (OCLC)
OCLC library identifier	AU@
System control number	000048656228
029 1# - (OCLC)
OCLC library identifier	DKDLA
System control number	820120-katalog:000462213
029 1# - (OCLC)
OCLC library identifier	DKDLA
System control number	820120-katalog:999919889205765
029 1# - (OCLC)
OCLC library identifier	NLGGC
System control number	384365841
029 1# - (OCLC)
OCLC library identifier	NZ1
System control number	13046002
035 ## - SYSTEM CONTROL NUMBER
System control number	(OCoLC)432712655
Canceled/invalid control number	(OCoLC)428884845
--	(OCoLC)432209626
--	(OCoLC)488556420
--	(OCoLC)613528865
--	(OCoLC)647818564
--	(OCoLC)880316574
--	(OCoLC)964932863
--	(OCoLC)1005835888
--	(OCoLC)1044245650
--	(OCoLC)1056378025
--	(OCoLC)1073061940
--	(OCoLC)1081244279
--	(OCoLC)1097279373
--	(OCoLC)1100827105
--	(OCoLC)1105596902
--	(OCoLC)1171539394
--	(OCoLC)1171846439
--	(OCoLC)1203991694
--	(OCoLC)1259224522
--	(OCoLC)1262684316
--	(OCoLC)1374612617
037 ## - SOURCE OF ACQUISITION
Stock number	978-3-642-02443-6
Source of stock number/acquisition	Springer
Note	http://www.springerlink.com
050 #4 - LIBRARY OF CONGRESS CALL NUMBER
Classification number	QA76.9.A96
Item number	T96 2008
072 #7 - SUBJECT CATEGORY CODE
Subject category code	UM
Source	bicssc
072 #7 - SUBJECT CATEGORY CODE
Subject category code	UYF
Source	bicssc
072 #7 - SUBJECT CATEGORY CODE
Subject category code	COM051000
Source	bisacsh
072 #7 - SUBJECT CATEGORY CODE
Subject category code	COM036000
Source	bisacsh
082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER
Classification number	005.131
Edition number	22
084 ## - OTHER CLASSIFICATION NUMBER
Classification number	SS 4800
Number source	rvk
084 ## - OTHER CLASSIFICATION NUMBER
Classification number	DAT 510f
Number source	stub
084 ## - OTHER CLASSIFICATION NUMBER
Classification number	DAT 706f
Number source	stub
084 ## - OTHER CLASSIFICATION NUMBER
Classification number	DAT 373f
Number source	stub
049 ## - LOCAL HOLDINGS (OCLC)
Holding library	MAIN
111 2# - MAIN ENTRY--MEETING NAME
Meeting name or jurisdiction name as entry element	TYPES 2008
Date of meeting	(2008 :
Location of meeting	Torino, Italy)
9 (RLIN)	35356
245 10 - TITLE STATEMENT
Title	Types for proofs and programs :
Remainder of title	international conference, TYPES 2008, Torino, Italy, March 26-29, 2008 : revised selected papers /
Statement of responsibility, etc.	Stefano Berardi, Ferruccio Damiani, Ugo de' Liguoro (eds.).
246 30 - VARYING FORM OF TITLE
Title proper/short title	TYPES 2008
260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT)
Place of publication, distribution, etc.	Berlin ;
--	New York :
Name of publisher, distributor, etc.	Springer,
Date of publication, distribution, etc.	2009.
300 ## - PHYSICAL DESCRIPTION
Extent	1 online resource (viii, 322 pages) :
Other physical details	illustrations
336 ## - CONTENT TYPE
Content type term	text
Content type code	txt
Source	rdacontent
337 ## - MEDIA TYPE
Media type term	computer
Media type code	c
Source	rdamedia
338 ## - CARRIER TYPE
Carrier type term	online resource
Carrier type code	cr
Source	rdacarrier
347 ## - DIGITAL FILE CHARACTERISTICS
File type	text file
347 ## - DIGITAL FILE CHARACTERISTICS
Encoding format	PDF
490 1# - SERIES STATEMENT
Series statement	Lecture notes in computer science,
International Standard Serial Number	0302-9743 ;
Volume/sequential designation	5497
490 1# - SERIES STATEMENT
Series statement	LNCS sublibrary: SL 1--Theoretical computer science and general issues
504 ## - BIBLIOGRAPHY, ETC. NOTE
Bibliography, etc	Includes bibliographical references and index.
588 0# - SOURCE OF DESCRIPTION NOTE
Source of description note	Print version record.
520 ## - SUMMARY, ETC.
Summary, etc.	This book constitutes the thoroughly refereed post-conference proceedings of TYPES 2008, the last of a series of meetings of the TYPES working group funded by the European Union between 1993 and 2008; the workshop has been held in Torino, Italy, in March 2008. The 19 revised full papers presented were carefully reviewed and selected from 27 submissions. The topic of the workshop was formal reasoning and computer programming based on type theory: languages and computerized tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, mobile code, formalization of mathematics, mathematics education.
505 0# - FORMATTED CONTENTS NOTE
Formatted contents note	Type Inference by Coinductive Logic Programming -- About the Formalization of Some Results by Chebyshev in Number Theory -- A New Elimination Rule for the Calculus of Inductive Constructions -- A Framework for the Analysis of Access Control Models for Interactive Mobile Devices -- Proving Infinitary Normalization -- First-Class Object Sets -- Monadic Translation of Intuitionistic Sequent Calculus -- Towards a Type Discipline for Answer Set Programming -- Type Inference for a Polynomial Lambda Calculus -- Local Theory Specifications in Isabelle/Isar -- Axiom Directed Focusing -- A Type System for Usage of Software Components -- Merging Procedural and Declarative Proof -- Using Structural Recursion for Corecursion -- Manifest Fields and Module Mechanisms in Intensional Type Theory -- A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq -- Coalgebraic Reasoning in Coq: Bisimulation and the?-Coiteration Scheme -- A Process-Model for Linear Programs -- Some Complexity and Expressiveness Results on Multimodal and Stratified Proof Nets.
546 ## - LANGUAGE NOTE
Language note	English.
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element	Automatic theorem proving
Form subdivision	Congresses.
9 (RLIN)	14919
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element	Computer programming
Form subdivision	Congresses.
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element	Théorèmes
General subdivision	Démonstration automatique
Form subdivision	Congrès.
9 (RLIN)	14921
650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element	Programmation (Informatique)
Form subdivision	Congrès.
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element	Informatique.
Source of heading or term	eclas
9 (RLIN)	14930
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element	Automatic theorem proving
Source of heading or term	fast
9 (RLIN)	14923
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element	Computer programming
Source of heading or term	fast
9 (RLIN)	3021
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element	Beweistheorie
Source of heading or term	gnd
9 (RLIN)	35358
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element	Programmierung
Source of heading or term	gnd
9 (RLIN)	5173
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element	Typentheorie
Source of heading or term	gnd
9 (RLIN)	35359
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element	Typsystem
Source of heading or term	gnd
9 (RLIN)	35360
650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element	HOL
Source of heading or term	gnd
9 (RLIN)	14931
655 #2 - INDEX TERM--GENRE/FORM
Genre/form data or focus term	Congress
9 (RLIN)	11670
655 #7 - INDEX TERM--GENRE/FORM
Genre/form data or focus term	proceedings (reports)
Source of term	aat
655 #7 - INDEX TERM--GENRE/FORM
Genre/form data or focus term	Conference papers and proceedings
Source of term	fast
9 (RLIN)	6065
655 #7 - INDEX TERM--GENRE/FORM
Genre/form data or focus term	Conference papers and proceedings.
Source of term	lcgft
9 (RLIN)	6065
655 #7 - INDEX TERM--GENRE/FORM
Genre/form data or focus term	Actes de congrès.
Source of term	rvmgf
9 (RLIN)	609890
655 #7 - INDEX TERM--GENRE/FORM
Genre/form data or focus term	Kongress.
Source of term	swd
9 (RLIN)	2843
655 #7 - INDEX TERM--GENRE/FORM
Genre/form data or focus term	Turin (2008)
Source of term	swd
9 (RLIN)	976417
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name	Berardi, Stefano.
9 (RLIN)	33915
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name	Damiani, Ferruccio.
9 (RLIN)	33917
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name	De'Liguoro, Ugo.
9 (RLIN)	35361
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Relationship information	Print version:
Main entry heading	TYPES 2008 (2008 : Torino, Italy).
Title	Types for proofs and programs.
Place, publisher, and date of publication	Berlin ; New York : Springer, 2009
International Standard Book Number	9783642024436
--	3642024432
Record control number	(OCoLC)423920154
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title	Lecture notes in computer science ;
Volume number/sequential designation	5497.
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title	LNCS sublibrary.
Number of part/section of a work	SL 1,
Name of part/section of a work	Theoretical computer science and general issues.
9 (RLIN)	20736
856 40 - ELECTRONIC LOCATION AND ACCESS
Uniform Resource Identifier	<a href="https://link.springer.com/10.1007/978-3-642-02444-3">https://link.springer.com/10.1007/978-3-642-02444-3</a>
938 ## -
--	ProQuest Ebook Central
--	EBLB
--	EBL3064272
938 ## -
--	ebrary
--	EBRY
--	ebr10310163
938 ## -
--	ProQuest MyiLibrary Digital eBook Collection
--	IDEB
--	cis23905682
938 ## -
--	YBP Library Services
--	YANK
--	3075278
994 ## -
--	92
--	ATIST

Holdings
Withdrawn status	Lost status	Damaged status	Not for loan	Collection code	Home library	Current library	Date acquired	Total Checkouts	Date last seen	Price effective from	Koha item type
	Not Lost			eBook LNCS	e-Library	e-Library	28/07/2022		28/07/2022	28/07/2022	eBook