Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings / Jean-Pierre Jouannaud, Zhong Shao (eds.). |
Creatore | [CPP (Conference) (1st : 2011 : Kʻen-ting, Taiwan)] |
Estensione | 1 online resource (xv, 399 pages). |
Disciplina | 004.01/51 |
Accesso persona |
Jouannaud, Jean-Pierre
Shao, Zhong, 1968- |
Genere/Forma |
Electronic books
Conference papers and proceedings |
Soggetto non controllato |
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) |
ISBN |
9783642253799
3642253792 9783642253782 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
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 |
Record Nr. | NYU-006478990 |
[CPP (Conference) (1st : 2011 : Kʻen-ting, Taiwan)]
![]() |
|
![]() | |
Lo trovi qui: New York University | |
Certified programs and proofs : third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings / edited by Georges Gonthier, Michael Norrish |
Creatore | [CPP (Conference) (3rd : 2013 : Melbourne, Vic.)] |
Estensione | 1 online resource (xii, 309 pages) : illustrations. |
Disciplina | 005.1015113 |
Accesso persona |
Gonthier, Georges, editor
Norrish, Michael, editor |
Genere/Forma |
Electronic books
Conference papers and proceedings Ebook Congresses |
ISBN |
9783319035451
3319035452 3319035444 9783319035444 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Invited Lectures -- [pi]n(Sn) in Homotopy Type Theory -- Session 1: Code Verification -- Mostly Sound Type System Improves a Foundational Program Verifier -- Computational Verification of Network Programs in Coq -- Aliasing Restrictions of C11 Formalized in Coq -- Session 2: Elegant Proofs -- Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code -- A Constructive Theory of Regular Languages in Coq -- Certified Parsing of Regular Languages -- Session 3: Proof Libraries -- Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory -- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL -- Refinements for Free! -- Session 4: Mathematics -- A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem -- Certified Kruskal's Tree Theorem -- Extracting Proofs from Tabled Proof Search -- Session 5: Certified Transformations -- Formalizing the SAFECode Type System -- Certifiably Sound Parallelizing Transformations -- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax -- Session 6: Security -- Formalizing Probabilistic Noninterference -- Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties -- A Formal Model and Correctness Proof for an Access Control Policy Framework.
Invited Lectures. π n (S n) in Homotopy Type Theory / Daniel R. Licata and Guillaume Brunerie -- Session 1: Code Verification. Mostly Sound Type System Improves a Foundational Program Verifier / Josiah Dodds and Andrew W. Appel -- Computational Verification of Network Programs in Coq / Gordon Stewart -- Aliasing Restrictions of C11 Formalized in Coq / Robbert Krebbers -- Session 2: Elegant Proofs. Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code / Magnus O. Myreen and Gregorio Curello -- A Constructive Theory of Regular Languages in Coq / Christian Doczkal, Jan-Oliver Kaiser and Gert Smolka -- Certified Parsing of Regular Languages / Denis Firsov and Tarmo Uustalu -- Session 3: Proof Libraries. Nonfree Datatypes in Isabelle/HOL / Andreas Schropp and Andrei Popescu -- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL / Brian Huffman and Ondřej Kunčar -- Refinements for Free! / Cyril Cohen, Maxime Dénès and Anders Mörtberg -- Session 4: Mathematics. A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem / Andrea Asperti -- Certified Kruskal's Tree Theorem / Christian Sternagel -- Extracting Proofs from Tabled Proof Search / Dale Miller and Alwen Tiu -- Session 5: Certified Transformations. Formalizing the SAFECode Type System / Daniel Huang and Greg Morrisett -- Certifiably Sound Parallelizing Transformations / Christian J. Bell -- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax / Olivier Savary-Belanger, Stefan Monnier and Brigitte Pientka -- Session 6: Security. Formalizing Probabilistic Noninterference / Andrei Popescu, Johannes Hölzl and Tobias Nipkow -- Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties / Narges Khakpour, Oliver Schwarz and Mads Dam -- A Formal Model and Correctness Proof for an Access Control Policy^ Framework / Chunhan Wu, Xingyuan Zhang and Christian Urban. |
Record Nr. | NYU-004669300 |
[CPP (Conference) (3rd : 2013 : Melbourne, Vic.)]
![]() |
|
![]() | |
Lo trovi qui: New York University | |
Certified programs and proofs [electronic resource] : first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings / Jean-Pierre Jouannaud, Zhong Shao (eds.). |
Creatore | [CPP (Conference) (1st : 2011 : Kʻen-ting, Taiwan)] |
Estensione | 1 online resource (xv, 399 p.) |
Disciplina | 004.01/51 |
Accesso persona |
Jouannaud, Jean-Pierre
Shao, Zhong, 1968- |
Genere/Forma | Electronic books |
Soggetto non controllato |
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) |
ISBN |
9783642253799 (electronic bk.)
3642253792 (electronic bk.) 9783642253782 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UPENN-9960089713503681 |
[CPP (Conference) (1st : 2011 : Kʻen-ting, Taiwan)]
![]() |
|
![]() | |
Lo trovi qui: University of Pennsylvania | |
Certified programs and proofs [electronic resource] : third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings / edited by Georges Gonthier, Michael Norrish |
Creatore | [CPP (Conference) (3rd : 2013 : Melbourne, Vic.)] |
Estensione | 1 online resource (xii, 309 pages) : illustrations |
Disciplina | 005.1015113 |
Accesso persona |
Gonthier, Georges, editor of compilation
Norrish, Michael, editor of compilation |
Genere/Forma | Electronic books |
ISBN |
9783319035451 (electronic bk.)
3319035452 (electronic bk.) 9783319035444 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UPENN-9962055803503681 |
[CPP (Conference) (3rd : 2013 : Melbourne, Vic.)]
![]() |
|
![]() | |
Lo trovi qui: University of Pennsylvania | |
Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings / Jean-Pierre Jouannaud, Zhong Shao (eds.). |
Creatore | [CPP (Conference) (1st : 2011 : Kʻen-ting, Taiwan)] |
Estensione | 1 online resource (xv, 399 pages). |
Disciplina | 004.01/51 |
Accesso persona |
Jouannaud, Jean-Pierre
Shao, Zhong, 1968- |
Soggetto non controllato |
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) |
ISBN |
9783642253799
3642253792 9783642253782 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
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 |
Record Nr. | STANFORD-a9408466 |
[CPP (Conference) (1st : 2011 : Kʻen-ting, Taiwan)]
![]() |
|
![]() | |
Lo trovi qui: Stanford University | |
Certified programs and proofs : third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings / edited by Georges Gonthier, Michael Norrish |
Creatore | [CPP (Conference) (3rd : 2013 : Melbourne, Vic.)] |
Estensione | 1 online resource (xii, 309 pages) : illustrations. |
Disciplina | 005.1015113 |
Accesso persona |
Gonthier, Georges, editor
Norrish, Michael, editor |
Genere/Forma |
Congresses
Electronic books Conference papers and proceedings |
ISBN |
9783319035451
3319035452 3319035444 9783319035444 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Invited Lectures -- [pi]n(Sn) in Homotopy Type Theory -- Session 1: Code Verification -- Mostly Sound Type System Improves a Foundational Program Verifier -- Computational Verification of Network Programs in Coq -- Aliasing Restrictions of C11 Formalized in Coq -- Session 2: Elegant Proofs -- Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code -- A Constructive Theory of Regular Languages in Coq -- Certified Parsing of Regular Languages -- Session 3: Proof Libraries -- Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory -- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL -- Refinements for Free! -- Session 4: Mathematics -- A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem -- Certified Kruskal's Tree Theorem -- Extracting Proofs from Tabled Proof Search -- Session 5: Certified Transformations -- Formalizing the SAFECode Type System -- Certifiably Sound Parallelizing Transformations -- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax -- Session 6: Security -- Formalizing Probabilistic Noninterference -- Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties -- A Formal Model and Correctness Proof for an Access Control Policy Framework.
Invited Lectures. π n (S n) in Homotopy Type Theory / Daniel R. Licata and Guillaume Brunerie -- Session 1: Code Verification. Mostly Sound Type System Improves a Foundational Program Verifier / Josiah Dodds and Andrew W. Appel -- Computational Verification of Network Programs in Coq / Gordon Stewart -- Aliasing Restrictions of C11 Formalized in Coq / Robbert Krebbers -- Session 2: Elegant Proofs. Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code / Magnus O. Myreen and Gregorio Curello -- A Constructive Theory of Regular Languages in Coq / Christian Doczkal, Jan-Oliver Kaiser and Gert Smolka -- Certified Parsing of Regular Languages / Denis Firsov and Tarmo Uustalu -- Session 3: Proof Libraries. Nonfree Datatypes in Isabelle/HOL / Andreas Schropp and Andrei Popescu -- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL / Brian Huffman and Ondřej Kunčar -- Refinements for Free! / |
Record Nr. | NYU-004444413 |
[CPP (Conference) (3rd : 2013 : Melbourne, Vic.)]
![]() |
|
![]() | |
Lo trovi qui: New York University | |
Certified programs and proofs : third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings / edited by Georges Gonthier, Michael Norrish |
Creatore | [CPP (Conference) (3rd : 2013 : Melbourne, Vic.)] |
Estensione | 1 online resource (xii, 309 pages) : illustrations. |
Accesso persona |
Gonthier, Georges, editor
Norrish, Michael, editor |
Genere/Forma |
Electronic books
Conference papers and proceedings Ebook Congresses |
ISBN |
9783319035451
3319035452 3319035444 9783319035444 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Lectures -- [pi]n(Sn) in Homotopy Type Theory -- Session 1: Code Verification -- Mostly Sound Type System Improves a Foundational Program Verifier -- Computational Verification of Network Programs in Coq -- Aliasing Restrictions of C11 Formalized in Coq -- Session 2: Elegant Proofs -- Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code -- A Constructive Theory of Regular Languages in Coq -- Certified Parsing of Regular Languages -- Session 3: Proof Libraries -- Nonfree Datatypes in Isabelle/HOL: Animating a Many-Sorted Metatheory -- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL -- Refinements for Free! -- Session 4: Mathematics -- A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem -- Certified Kruskal's Tree Theorem -- Extracting Proofs from Tabled Proof Search -- Session 5: Certified Transformations -- Formalizing the SAFECode Type System -- Certifiably Sound Parallelizing Transformations -- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax -- Session 6: Security -- Formalizing Probabilistic Noninterference -- Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties -- A Formal Model and Correctness Proof for an Access Control Policy Framework. |
Record Nr. | UCHICAGO-11083926 |
[CPP (Conference) (3rd : 2013 : Melbourne, Vic.)]
![]() |
|
![]() | |
Lo trovi qui: University of Chicago | |
Certified programs and proofs : first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings / Jean-Pierre Jouannaud, Zhong Shao (eds.). |
Creatore | [CPP (Conference) (1st : 2011 : Kʻen-ting, Taiwan)] |
Estensione | 1 online resource (xv, 399 pages). |
Disciplina | 004.01/51 |
Accesso persona |
Jouannaud, Jean-Pierre
Shao, Zhong, 1968- |
Genere/Forma |
Electronic books
Conference papers and proceedings |
Soggetto non controllato |
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) |
ISBN |
9783642253799
3642253792 9783642253782 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | NYU-004372514 |
[CPP (Conference) (1st : 2011 : Kʻen-ting, Taiwan)]
![]() |
|
![]() | |
Lo trovi qui: New York University | |
Certified programs and proofs : third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings / edited by Georges Gonthier, Michael Norrish |
Creatore | [CPP (Conference) (3rd : 2013 : Melbourne, Vic.)] |
Estensione | 1 online resource (xii, 309 pages) : illustrations. |
Disciplina | 005.1015113 |
Accesso persona |
Gonthier, Georges, editor of compilation
Norrish, Michael, editor of compilation |
Accesso convegno | CPP (Conference) |
ISBN |
9783319035451 (electronic bk.)
3319035452 (electronic bk.) 9783319035444 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UALBERTA-6537158 |
[CPP (Conference) (3rd : 2013 : Melbourne, Vic.)]
![]() |
|
![]() | |
Lo trovi qui: University of Alberta / NEOS Library Consortium | |
CPP '15 [electronic resource] : proceedings of the 2015 ACM Conference on Certified Programs and Proofs : January 13-14, 2015, Mumbai, India / sponsored by ACM SIGPLAN |
Creatore | [CPP (Conference) (4th : 2015 : Mumbai, India)] |
Estensione | 1 online resource (1 online resource (184 pages)) |
Accesso ente | ACM Special Interest Group on Programming Languages |
Genere/Forma | Electronic books |
ISBN | 9781450332965 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | DUKE-007462893 |
[CPP (Conference) (4th : 2015 : Mumbai, India)]
![]() |
|
![]() | |
Lo trovi qui: Duke University | |