top

  Info

  • Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.
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
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.)]  
Materiale a stampa
Lo trovi qui: University of Pennsylvania
Certified programs and proofs [electronic resource] : first International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings / Jean-Pierre Jouannaud, Zhong Shao (eds.).
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)]  
Materiale a stampa
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.).
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)]  
Materiale a stampa
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
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.)]  
Materiale a stampa
Lo trovi qui: New York University
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.).
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)]  
Materiale a stampa
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
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.)]  
Materiale a stampa
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
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.)]  
Materiale a stampa
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.).
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)]  
Materiale a stampa
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
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.)]  
Materiale a stampa
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
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)]  
Materiale a stampa
Lo trovi qui: Duke University