06720cam a2200865Ka 4500
ocn761874772
OCoLC
20200626111942.0
m o d
cr cnu---unuuu
111122s2011 gw ob 101 0 eng d
GW5XE
eng
pn
GW5XE
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
015975120
Uk
846870049
9783642253799
(electronic bk.)
3642253792
(electronic bk.)
9783642253782
10.1007/978-3-642-25379-9
doi
AU@
000048657253
AU@
000051318685
AU@
000058159035
AU@
000060505263
DKDLA
820120-katalog:000687128
NLGGC
384338046
NZ1
14154156
(OCoLC)761874772
(OCoLC)846870049
QA76.9.M35
C37 2011eb
UM
bicssc
UYF
bicssc
COM051000
bisacsh
COM036000
bisacsh
004.01/51
23
MAIN
CPP (Conference)
(1st :
2011 :
Kʻen-ting, Taiwan)
43482
Certified programs and proofs :
first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings /
Jean-Pierre Jouannaud, Zhong Shao (eds.).
Berlin ;
New York :
Springer,
©2011.
1 online resource (xv, 399 pages)
text
txt
rdacontent
computer
c
rdamedia
online resource
cr
rdacarrier
text file
PDF
rda
Lecture notes in computer science,
0302-9743 ;
7086
LNCS sublibrary. SL 1, Theoretical computer science and general issues
Serienbezeichnung
Includes bibliographical references and author index.
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.
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
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
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
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
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
Computer science
Mathematics
Congresses.
15039
Informatique.
eclas
14930
Computer science
Mathematics.
fast
(OCoLC)fst00872460
2386
Computer science
Software engineering
Logic design
Artificial intelligence
Logics and Meanings of Programs
Mathematical Logic and Formal Languages
Programming Languages, Compilers, Interpreters
Symbolic and Algebraic Manipulation
Artificial Intelligence (incl. Robotics)
Electronic books.
396
Conference papers and proceedings.
fast
(OCoLC)fst01423772
6065
Jouannaud, Jean-Pierre.
22115
Shao, Zhong,
1968-
23984
Printed edition:
9783642253782
Lecture notes in computer science ;
7086.
43483
LNCS sublibrary.
SL 1,
Theoretical computer science and general issues.
20736
https://link-springer-com.libraryproxy.ist.ac.at/book/10.1007/978-3-642-25379-9
ProQuest Ebook Central
EBLB
EBL5584955
YBP Library Services
YANK
7274781
92
ATIST
381846
381846
0
0
0
0
EBook
elib
elib
2020-06-26
2020-06-26
2020-06-26
EBOOK