The Resource Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 79, 2011. Proceedings, JeanPierre Jouannaud, Zhong Shao (eds.)
Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 79, 2011. Proceedings, JeanPierre Jouannaud, Zhong Shao (eds.)
Resource Information
The item Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 79, 2011. Proceedings, JeanPierre Jouannaud, Zhong Shao (eds.) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries.This item is available to borrow from 2 library branches.
Resource Information
The item Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 79, 2011. Proceedings, JeanPierre Jouannaud, Zhong Shao (eds.) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries.
This item is available to borrow from 2 library branches.
 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
 Language
 eng
 Extent
 1 online resource (xv, 399 pages).
 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; ProofCarrying Code in a SessionTyped 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; NonMatrix 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; PseudoDivision and PseudoRemainder; 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 ContextFree 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 PrefixSoundness; Completeness and PrefixCompleteness; Parser Generator Completeness; Implementation Issues; Related Work; Conclusion; References; A Decision Procedure for Regular Expression Equivalence in Type Theory
 Isbn
 9783642253799
 Label
 Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 79, 2011. Proceedings
 Title
 Certified programs and proofs
 Title remainder
 first International Conference, CPP 2011, Kenting, Taiwan, December 79, 2011. Proceedings
 Statement of responsibility
 JeanPierre Jouannaud, Zhong Shao (eds.)
 Subject

 Artificial intelligence
 Computer science
 Computer science  Mathematics
 Computer science  Mathematics
 Computer science  Mathematics  Congresses
 Conference papers and proceedings
 Conference papers and proceedings
 Informatique
 Logic design
 Logics and Meanings of Programs
 Mathematical Logic and Formal Languages
 Programming Languages, Compilers, Interpreters
 Software engineering
 Symbolic and Algebraic Manipulation
 Artificial Intelligence (incl. Robotics)
 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
 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, JeanPierre
 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 79, 2011. Proceedings, JeanPierre Jouannaud, Zhong Shao (eds.)
 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; ProofCarrying Code in a SessionTyped 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; NonMatrix 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; PseudoDivision and PseudoRemainder; 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 ContextFree 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 PrefixSoundness; Completeness and PrefixCompleteness; 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/9783642253799
 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 79, 2011. Proceedings, JeanPierre Jouannaud, Zhong Shao (eds.)
 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; ProofCarrying Code in a SessionTyped 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; NonMatrix 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; PseudoDivision and PseudoRemainder; 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 ContextFree 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 PrefixSoundness; Completeness and PrefixCompleteness; 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/9783642253799
 Quality assurance targets
 not applicable
 Reformatting quality
 unknown
 Sound
 unknown sound
 Specific material designation
 remote
 System control number
 (OCoLC)761874772
Subject
 Artificial intelligence
 Computer science
 Computer science  Mathematics
 Computer science  Mathematics
 Computer science  Mathematics  Congresses
 Conference papers and proceedings
 Conference papers and proceedings
 Informatique
 Logic design
 Logics and Meanings of Programs
 Mathematical Logic and Formal Languages
 Programming Languages, Compilers, Interpreters
 Software engineering
 Symbolic and Algebraic Manipulation
 Artificial Intelligence (incl. Robotics)
Genre
Member of
 LNCS sublibrary, SL 1, Theoretical computer science and general issues
 Lecture notes in computer science, 7086
Library Links
Embed
Settings
Select options that apply then copy and paste the RDF/HTML data fragment to include in your application
Embed this data in a secure (HTTPS) page:
Layout options:
Include data citation:
<div class="citation" vocab="http://schema.org/"><i class="fa faexternallinksquare fafw"></i> Data from <span resource="http://link.library.missouri.edu/portal/Certifiedprogramsandproofsfirst/5v4WrKEFowE/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.library.missouri.edu/portal/Certifiedprogramsandproofsfirst/5v4WrKEFowE/">Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 79, 2011. Proceedings, JeanPierre Jouannaud, Zhong Shao (eds.)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.library.missouri.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.library.missouri.edu/">University of Missouri Libraries</a></span></span></span></span></div>
Note: Adjust the width and height settings defined in the RDF/HTML code fragment to best match your requirements
Preview
Cite Data  Experimental
Data Citation of the Item Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 79, 2011. Proceedings, JeanPierre Jouannaud, Zhong Shao (eds.)
Copy and paste the following RDF/HTML data fragment to cite this resource
<div class="citation" vocab="http://schema.org/"><i class="fa faexternallinksquare fafw"></i> Data from <span resource="http://link.library.missouri.edu/portal/Certifiedprogramsandproofsfirst/5v4WrKEFowE/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.library.missouri.edu/portal/Certifiedprogramsandproofsfirst/5v4WrKEFowE/">Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 79, 2011. Proceedings, JeanPierre Jouannaud, Zhong Shao (eds.)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.library.missouri.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.library.missouri.edu/">University of Missouri Libraries</a></span></span></span></span></div>