Certified programs and proofs : (Record no. 381846)

000 -LEADER
fixed length control field 06720cam a2200865Ka 4500
001 - CONTROL NUMBER
control field ocn761874772
003 - CONTROL NUMBER IDENTIFIER
control field OCoLC
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20200626111942.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 cnu---unuuu
008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION
fixed length control field 111122s2011 gw ob 101 0 eng d
040 ## - CATALOGING SOURCE
Original cataloging agency GW5XE
Language of cataloging eng
Description conventions pn
Transcribing agency GW5XE
Modifying agency UKMGB
-- COO
-- VRC
-- OCLCQ
-- OCLCA
-- OCLCF
-- BEDGE
-- DKDLA
-- OCLCQ
-- OCLCO
-- YDXCP
-- AU@
-- NUI
-- OCL
-- OCLCO
-- OCLCQ
-- VGM
-- ESU
-- OCLCQ
-- VT2
-- SHS
-- IOG
-- BUF
-- CEF
-- U3W
-- EBLCP
-- WYU
-- YOU
-- CNTRU
-- OCLCQ
016 7# - NATIONAL BIBLIOGRAPHIC AGENCY CONTROL NUMBER
Record control number 015975120
Source Uk
019 ## -
-- 846870049
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9783642253799
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 3642253792
Qualifying information (electronic bk.)
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
Canceled/invalid ISBN 9783642253782
024 7# - OTHER STANDARD IDENTIFIER
Standard number or code 10.1007/978-3-642-25379-9
Source of number or code doi
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000048657253
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000051318685
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000058159035
029 1# - (OCLC)
OCLC library identifier AU@
System control number 000060505263
029 1# - (OCLC)
OCLC library identifier DKDLA
System control number 820120-katalog:000687128
029 1# - (OCLC)
OCLC library identifier NLGGC
System control number 384338046
029 1# - (OCLC)
OCLC library identifier NZ1
System control number 14154156
035 ## - SYSTEM CONTROL NUMBER
System control number (OCoLC)761874772
Canceled/invalid control number (OCoLC)846870049
050 #4 - LIBRARY OF CONGRESS CALL NUMBER
Classification number QA76.9.M35
Item number C37 2011eb
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 004.01/51
Edition number 23
049 ## - LOCAL HOLDINGS (OCLC)
Holding library MAIN
111 2# - MAIN ENTRY--MEETING NAME
Meeting name or jurisdiction name as entry element CPP (Conference)
Number of part/section/meeting (1st :
Date of meeting 2011 :
Location of meeting Kʻen-ting, Taiwan)
9 (RLIN) 43482
245 10 - TITLE STATEMENT
Title Certified programs and proofs :
Remainder of title first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings /
Statement of responsibility, etc. Jean-Pierre Jouannaud, Zhong Shao (eds.).
260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT)
Place of publication, distribution, etc. Berlin ;
-- New York :
Name of publisher, distributor, etc. Springer,
Date of publication, distribution, etc. ©2011.
300 ## - PHYSICAL DESCRIPTION
Extent 1 online resource (xv, 399 pages)
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
Encoding format PDF
Source rda
490 1# - SERIES STATEMENT
Series statement Lecture notes in computer science,
International Standard Serial Number 0302-9743 ;
Volume/sequential designation 7086
490 1# - SERIES STATEMENT
Series statement LNCS sublibrary. SL 1, Theoretical computer science and general issues
490 ## - SERIES STATEMENT
Series statement Serienbezeichnung
504 ## - BIBLIOGRAPHY, ETC. NOTE
Bibliography, etc Includes bibliographical references and author index.
520 8# - SUMMARY, ETC.
Summary, etc. Annotation This book constitutes the referred proceedings of the First International Conference on Certified Programs and Proofs, CPP 2011, held in Kenting, Taiwan, in December 2011. The 24 revised regular papers presented together with 4 invited talks were carefully reviewed and selected from 49 submissions. They are organized in topical sections on logic and types, certificates, formalization, proof assistants, teaching, programming languages, hardware certification, miscellaneous, and proof perls.
505 0# - FORMATTED CONTENTS NOTE
Formatted contents note Intro; Title; Preface; Organization; Table of Contents; APLAS/CPP Invited Talks; Engineering Theories with Z3; Introduction; References; Algebra, Logic, Locality, Concurrency; References; Session 1: Logic and Types; Constructive Formalization of Hybrid Logic with Eventualities; Introduction; Propositional Logic; Mathematical Development; Decidability, Finite Types and Finite Sets; Formalization of Propositional Logic; Modal Logic; Mathematical Development; Demo Theorem; Formalization of Modal Logic; Hybrid Logic; Mathematical Development; Demo Theorem for Hybrid Logic
505 8# - FORMATTED CONTENTS NOTE
Formatted contents note Formalization of Hybrid LogicConclusions; References; Proof-Carrying Code in a Session-Typed Process Calculus; Introduction; Dependent Session Types; Proof Irrelevance; Affirmation; Progress and Preservation; Concluding Remarks; References; Session 2: Certificates; Automated Certification of Implicit Induction Proofs; Introduction; Background and Notations; Noetherian Induction for Implicit Induction Proofs; Case Study: Validation of a Conformance Algorithm for the ABR Protocol; The Spike Specification; An Example of Implicit Induction Proof; Certifying Implicit Induction Proofs
505 8# - FORMATTED CONTENTS NOTE
Formatted contents note ImprovementsConclusions and Future Work; References; A Proposal for Broad Spectrum Proof Certificates; Introduction; Proof Theory and Proof Certificates; The Basics of Sequent Calculus; Encoding Computation with the Sequent Calculus; Focused Proof Systems; LKF: A Focused Proof System for Classical Logic; Positive and Negative Macro Inference Rules; Some Examples of Proof Certificates; Non-Matrix Proof Systems; Fixed Points and Equality; Computation and Model Checking; Related Work; Future Work; Conclusion; References; Session 3: Invited Talk
505 8# - FORMATTED CONTENTS NOTE
Formatted contents note Univalent Semantics of Constructive Type TheoriesSession 4: Formalization; Formalization of Wu's Simple Method in Coq; Introduction; Related Work; Overview of Wu's Method; Cartesian Geometry; Rings and Ideals; Pseudo-Division and Pseudo-Remainder; Formalization in Coq; Algebraization; Certified Implementation; Benchmark; Conclusion; References; Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem; Introduction; Nominal Logic Preliminaries; Lambda Terms and Conversion; Defining -Constants with Nominal Isabelle; Basic Constants in -Calculus
505 8# - FORMATTED CONTENTS NOTE
Formatted contents note The Proof of the Second Fixed Point TheoremConclusion; Related Work; References; Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars; Introduction; Types and Substrings; Grammars and Parse Trees; Parse Trees and the Parsing Context; Terminal Parsers and Parser Combinators; Updating the Parsing Context; Termination, Soundness and Prefix-Soundness; Completeness and Prefix-Completeness; Parser Generator Completeness; Implementation Issues; Related Work; Conclusion; References; A Decision Procedure for Regular Expression Equivalence in Type Theory
650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM
Topical term or geographic name as entry element Computer science
General subdivision Mathematics
Form subdivision Congresses.
9 (RLIN) 15039
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 Computer science
General subdivision Mathematics.
Source of heading or term fast
Authority record control number (OCoLC)fst00872460
9 (RLIN) 2386
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Computer science
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Software engineering
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Logic design
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Artificial intelligence
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Logics and Meanings of Programs
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Mathematical Logic and Formal Languages
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Programming Languages, Compilers, Interpreters
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Symbolic and Algebraic Manipulation
653 #4 - INDEX TERM--UNCONTROLLED
Uncontrolled term Artificial Intelligence (incl. Robotics)
655 #4 - INDEX TERM--GENRE/FORM
Genre/form data or focus term Electronic books.
9 (RLIN) 396
655 #7 - INDEX TERM--GENRE/FORM
Genre/form data or focus term Conference papers and proceedings.
Source of term fast
Authority record control number (OCoLC)fst01423772
9 (RLIN) 6065
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Jouannaud, Jean-Pierre.
9 (RLIN) 22115
700 1# - ADDED ENTRY--PERSONAL NAME
Personal name Shao, Zhong,
Dates associated with a name 1968-
9 (RLIN) 23984
776 08 - ADDITIONAL PHYSICAL FORM ENTRY
Relationship information Printed edition:
International Standard Book Number 9783642253782
830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE
Uniform title Lecture notes in computer science ;
Volume number/sequential designation 7086.
9 (RLIN) 43483
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.libraryproxy.ist.ac.at/book/10.1007/978-3-642-25379-9">https://link-springer-com.libraryproxy.ist.ac.at/book/10.1007/978-3-642-25379-9</a>
938 ## -
-- ProQuest Ebook Central
-- EBLB
-- EBL5584955
938 ## -
-- YBP Library Services
-- YANK
-- 7274781
994 ## -
-- 92
-- ATIST
Holdings
Withdrawn status Lost status Damaged status Not for loan Collection code Permanent Location Current Location Date acquired Date last seen Price effective from Koha item type
  Not Lost     EBook e-Library e-Library 2020-06-26 2020-06-26 2020-06-26 eBook

Powered by Koha