Coverart for item
The Resource Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, Jean-Pierre Jouannaud, Zhong Shao (eds.)

Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, Jean-Pierre Jouannaud, Zhong Shao (eds.)

Label
Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings
Title
Certified programs and proofs
Title remainder
first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings
Statement of responsibility
Jean-Pierre Jouannaud, Zhong Shao (eds.)
Creator
Contributor
Subject
Genre
Language
eng
Summary
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
Member of
Cataloging source
GW5XE
Dewey number
004.01/51
Index
index present
LC call number
QA76.9.M35
LC item number
C37 2011eb
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2011
http://bibfra.me/vocab/lite/meetingName
CPP (Conference)
Nature of contents
  • dictionaries
  • bibliography
http://library.link/vocab/relatedWorkOrContributorDate
1968-
http://library.link/vocab/relatedWorkOrContributorName
  • Jouannaud, Jean-Pierre
  • Shao, Zhong
Series statement
  • Lecture notes in computer science,
  • LNCS sublibrary. SL 1, Theoretical computer science and general issues
Series volume
7086
http://library.link/vocab/subjectName
  • Computer science
  • Informatique
  • Computer science
Label
Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, Jean-Pierre Jouannaud, Zhong Shao (eds.)
Instantiates
Publication
Antecedent source
unknown
Bibliography note
Includes bibliographical references and author index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
  • 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
Control code
761874772
Dimensions
unknown
Extent
1 online resource (xv, 399 pages).
File format
unknown
Form of item
online
Isbn
9783642253799
Level of compression
unknown
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
10.1007/978-3-642-25379-9
Quality assurance targets
not applicable
Reformatting quality
unknown
Sound
unknown sound
Specific material designation
remote
System control number
(OCoLC)761874772
Label
Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, Jean-Pierre Jouannaud, Zhong Shao (eds.)
Publication
Antecedent source
unknown
Bibliography note
Includes bibliographical references and author index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
  • 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
Control code
761874772
Dimensions
unknown
Extent
1 online resource (xv, 399 pages).
File format
unknown
Form of item
online
Isbn
9783642253799
Level of compression
unknown
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
10.1007/978-3-642-25379-9
Quality assurance targets
not applicable
Reformatting quality
unknown
Sound
unknown sound
Specific material designation
remote
System control number
(OCoLC)761874772

Library Locations

    • Ellis LibraryBorrow it
      1020 Lowry Street, Columbia, MO, 65201, US
      38.944491 -92.326012
    • Engineering Library & Technology CommonsBorrow it
      W2001 Lafferre Hall, Columbia, MO, 65211, US
      38.946102 -92.330125
Processing Feedback ...