Borrow it
 African Studies Library
 Alumni Medical Library
 Astronomy Library
 Fineman and Pappas Law Libraries
 Frederick S. Pardee Management Library
 Howard Gotlieb Archival Research Center
 Mugar Memorial Library
 Music Library
 Pikering Educational Resources Library
 School of Theology Library
 Science & Engineering Library
 Stone Science Library
The Resource Interactive theorem proving : 5th International Conference, ITP 2014, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 1417, 2014 : proceedings, Gerwin Klein, Ruben Gamboa (Eds.)
Interactive theorem proving : 5th International Conference, ITP 2014, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 1417, 2014 : proceedings, Gerwin Klein, Ruben Gamboa (Eds.)
Resource Information
The item Interactive theorem proving : 5th International Conference, ITP 2014, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 1417, 2014 : proceedings, Gerwin Klein, Ruben Gamboa (Eds.) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in Boston University Libraries.This item is available to borrow from all library branches.
Resource Information
The item Interactive theorem proving : 5th International Conference, ITP 2014, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 1417, 2014 : proceedings, Gerwin Klein, Ruben Gamboa (Eds.) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in Boston University Libraries.
This item is available to borrow from all library branches.
 Summary
 This book constitutes the proceedings of the 5th International Conference on Interactive Theorem Proving, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 35 papers presented in this volume were carefully reviewed and selected from 59 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematics
 Language
 eng
 Extent
 1 online resource (xxii, 555 pages)
 Note

 International conference proceedings
 Includes author index
 Contents

 Microcode Verification – Another Piece of the Microprocessor Verification Puzzle
 Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK
 Towards a Formally Verified Proof Assistant
 Implicational Rewriting Tactics in HOL
 A Heuristic Prover for Real Inequalities
 A Formal Library for Elliptic Curves in the Coq Proof Assistant
 Truly Modular (Co) data types for Isabelle/HOL
 Cardinals in Isabelle/HOL
 Verified Abstract Interpretation Techniques for Disassembling Lowlevel Selfmodifying Code
 Showing Invariance Compositionally for a Process Algebra for Network Protocols
 A ComputerAlgebraBased Formal Proof of the Irrationality of ζ(3)
 From Operational Models to Information Theory; Side Channels in pGCL with Isabelle
 A Coq Formalization of Finitely Presented Modules
 Formalized, Effective Domain Theory in Coq
 Completeness and Decidability Results for CTL in Coq
 Hypermap Specification and Certified Linked Implementation Using Orbits
 A Verified GenerateTestAggregate Coq Library for Parallel Programs Extraction
 Experience Implementing a Performant CategoryTheory Library in Coq
 A New and Formalized Proof of Abstract Completion
 HOL with Definitions: Semantics, Soundness and a Verified Implementation
 Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
 Recursive Functions on Lazy Lists via Domains and Topologies
 Formal Verification of Optical Quantum Flip Gate
 Compositional Computational Reflection
 An Isabelle Proof Method Language
 Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete
 The Reflective Milawa Theorem Prover Is Sound (Down to the Machine Code That Runs It)
 Balancing Lists: A Proof Pearl
 Unified Decision Procedures for Regular Expression Equivalence
 Collaborative Interactive Theorem Proving with Clide
 On the Formalization of ZTransform in HOL
 Universe Polymorphism in Coq
 Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
 HOL Constant Definition Done Right
 Rough Diamond: An Extension of EquivalenceBased Rewriting
 Formal C Semantics: Comp Cert and the C Standard
 Mechanical Certification of Loop Pipelining Transformations: A Preview
 Isbn
 9783319089706
 Label
 Interactive theorem proving : 5th International Conference, ITP 2014, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 1417, 2014 : proceedings
 Title
 Interactive theorem proving
 Title remainder
 5th International Conference, ITP 2014, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 1417, 2014 : proceedings
 Statement of responsibility
 Gerwin Klein, Ruben Gamboa (Eds.)
 Title variation
 ITP 2014
 Subject

 Automatic theorem proving  Congresses
 Conference proceedings
 Electronic resources
 Logic, Symbolic and mathematical
 Logic, Symbolic and mathematical  Congresses
 Logic, Symbolic and mathematical  Congresses
 Logic, Symbolic and mathematical  Congresses
 Automatic theorem proving  Congresses
 Automatic theorem proving  Congresses
 Automatic theorem proving
 Language
 eng
 Summary
 This book constitutes the proceedings of the 5th International Conference on Interactive Theorem Proving, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 35 papers presented in this volume were carefully reviewed and selected from 59 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematics
 Cataloging source
 NLGGC
 Government publication
 unknown if item is government publication
 Image bit depth
 0
 LC call number
 QA76.9.A96
 Literary form
 non fiction
 http://bibfra.me/vocab/lite/meetingDate
 2014
 http://bibfra.me/vocab/lite/meetingName
 ITP (Conference)
 Nature of contents
 dictionaries
 http://library.link/vocab/relatedWorkOrContributorName

 SpringerLink
 Klein, Gerwin
 Gamboa, Ruben
 Series statement
 Lecture Notes in Computer Science,
 Series volume
 8558
 http://library.link/vocab/subjectName

 Automatic theorem proving
 Logic, Symbolic and mathematical
 Automatic theorem proving
 Logic, Symbolic and mathematical
 Label
 Interactive theorem proving : 5th International Conference, ITP 2014, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 1417, 2014 : proceedings, Gerwin Klein, Ruben Gamboa (Eds.)
 Note

 International conference proceedings
 Includes author index
 Antecedent source
 mixed
 Carrier category
 online resource
 Carrier category code

 cr
 Carrier MARC source
 rdacarrier
 Color
 not applicable
 Content category
 text
 Content type code

 txt
 Content type MARC source
 rdacontent
 Contents
 Microcode Verification – Another Piece of the Microprocessor Verification Puzzle  Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK  Towards a Formally Verified Proof Assistant  Implicational Rewriting Tactics in HOL  A Heuristic Prover for Real Inequalities  A Formal Library for Elliptic Curves in the Coq Proof Assistant  Truly Modular (Co) data types for Isabelle/HOL  Cardinals in Isabelle/HOL  Verified Abstract Interpretation Techniques for Disassembling Lowlevel Selfmodifying Code  Showing Invariance Compositionally for a Process Algebra for Network Protocols  A ComputerAlgebraBased Formal Proof of the Irrationality of ζ(3)  From Operational Models to Information Theory; Side Channels in pGCL with Isabelle  A Coq Formalization of Finitely Presented Modules  Formalized, Effective Domain Theory in Coq  Completeness and Decidability Results for CTL in Coq  Hypermap Specification and Certified Linked Implementation Using Orbits  A Verified GenerateTestAggregate Coq Library for Parallel Programs Extraction  Experience Implementing a Performant CategoryTheory Library in Coq  A New and Formalized Proof of Abstract Completion  HOL with Definitions: Semantics, Soundness and a Verified Implementation  Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm  Recursive Functions on Lazy Lists via Domains and Topologies  Formal Verification of Optical Quantum Flip Gate  Compositional Computational Reflection  An Isabelle Proof Method Language  Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete  The Reflective Milawa Theorem Prover Is Sound (Down to the Machine Code That Runs It)  Balancing Lists: A Proof Pearl  Unified Decision Procedures for Regular Expression Equivalence  Collaborative Interactive Theorem Proving with Clide  On the Formalization of ZTransform in HOL  Universe Polymorphism in Coq  Asynchronous User Interaction and Tool Integration in Isabelle/PIDE  HOL Constant Definition Done Right  Rough Diamond: An Extension of EquivalenceBased Rewriting  Formal C Semantics: Comp Cert and the C Standard  Mechanical Certification of Loop Pipelining Transformations: A Preview
 Dimensions
 unknown
 Extent
 1 online resource (xxii, 555 pages)
 File format
 multiple file formats
 Form of item

 online
 electronic
 Isbn
 9783319089706
 Level of compression
 uncompressed
 Media category
 computer
 Media MARC source
 rdamedia
 Media type code

 c
 Other control number
 10.1007/9783319089706
 Other physical details
 illustrations.
 Quality assurance targets
 absent
 Reformatting quality
 access
 Specific material designation
 remote
 System control number

 (OCoLC)882248481
 (OCoLC)ocn882248481
 Label
 Interactive theorem proving : 5th International Conference, ITP 2014, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 1417, 2014 : proceedings, Gerwin Klein, Ruben Gamboa (Eds.)
 Note

 International conference proceedings
 Includes author index
 Antecedent source
 mixed
 Carrier category
 online resource
 Carrier category code

 cr
 Carrier MARC source
 rdacarrier
 Color
 not applicable
 Content category
 text
 Content type code

 txt
 Content type MARC source
 rdacontent
 Contents
 Microcode Verification – Another Piece of the Microprocessor Verification Puzzle  Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK  Towards a Formally Verified Proof Assistant  Implicational Rewriting Tactics in HOL  A Heuristic Prover for Real Inequalities  A Formal Library for Elliptic Curves in the Coq Proof Assistant  Truly Modular (Co) data types for Isabelle/HOL  Cardinals in Isabelle/HOL  Verified Abstract Interpretation Techniques for Disassembling Lowlevel Selfmodifying Code  Showing Invariance Compositionally for a Process Algebra for Network Protocols  A ComputerAlgebraBased Formal Proof of the Irrationality of ζ(3)  From Operational Models to Information Theory; Side Channels in pGCL with Isabelle  A Coq Formalization of Finitely Presented Modules  Formalized, Effective Domain Theory in Coq  Completeness and Decidability Results for CTL in Coq  Hypermap Specification and Certified Linked Implementation Using Orbits  A Verified GenerateTestAggregate Coq Library for Parallel Programs Extraction  Experience Implementing a Performant CategoryTheory Library in Coq  A New and Formalized Proof of Abstract Completion  HOL with Definitions: Semantics, Soundness and a Verified Implementation  Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm  Recursive Functions on Lazy Lists via Domains and Topologies  Formal Verification of Optical Quantum Flip Gate  Compositional Computational Reflection  An Isabelle Proof Method Language  Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete  The Reflective Milawa Theorem Prover Is Sound (Down to the Machine Code That Runs It)  Balancing Lists: A Proof Pearl  Unified Decision Procedures for Regular Expression Equivalence  Collaborative Interactive Theorem Proving with Clide  On the Formalization of ZTransform in HOL  Universe Polymorphism in Coq  Asynchronous User Interaction and Tool Integration in Isabelle/PIDE  HOL Constant Definition Done Right  Rough Diamond: An Extension of EquivalenceBased Rewriting  Formal C Semantics: Comp Cert and the C Standard  Mechanical Certification of Loop Pipelining Transformations: A Preview
 Dimensions
 unknown
 Extent
 1 online resource (xxii, 555 pages)
 File format
 multiple file formats
 Form of item

 online
 electronic
 Isbn
 9783319089706
 Level of compression
 uncompressed
 Media category
 computer
 Media MARC source
 rdamedia
 Media type code

 c
 Other control number
 10.1007/9783319089706
 Other physical details
 illustrations.
 Quality assurance targets
 absent
 Reformatting quality
 access
 Specific material designation
 remote
 System control number

 (OCoLC)882248481
 (OCoLC)ocn882248481
Subject
 Automatic theorem proving  Congresses
 Conference proceedings
 Electronic resources
 Logic, Symbolic and mathematical
 Logic, Symbolic and mathematical  Congresses
 Logic, Symbolic and mathematical  Congresses
 Logic, Symbolic and mathematical  Congresses
 Automatic theorem proving  Congresses
 Automatic theorem proving  Congresses
 Automatic theorem proving
Genre
Member of
Library Locations

African Studies LibraryBorrow it771 Commonwealth Avenue, 6th Floor, Boston, MA, 02215, US42.350723 71.108227


Astronomy LibraryBorrow it725 Commonwealth Avenue, 6th Floor, Boston, MA, 02445, US42.350259 71.105717

Fineman and Pappas Law LibrariesBorrow it765 Commonwealth Avenue, Boston, MA, 02215, US42.350979 71.107023

Frederick S. Pardee Management LibraryBorrow it595 Commonwealth Avenue, Boston, MA, 02215, US42.349626 71.099547

Howard Gotlieb Archival Research CenterBorrow it771 Commonwealth Avenue, 5th Floor, Boston, MA, 02215, US42.350723 71.108227


Music LibraryBorrow it771 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US42.350723 71.108227

Pikering Educational Resources LibraryBorrow it2 Silber Way, Boston, MA, 02215, US42.349804 71.101425

School of Theology LibraryBorrow it745 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US42.350494 71.107235

Science & Engineering LibraryBorrow it38 Cummington Mall, Boston, MA, 02215, US42.348472 71.102257

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.bu.edu/portal/Interactivetheoremproving5thInternational/mzrFxPlhC8E/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.bu.edu/portal/Interactivetheoremproving5thInternational/mzrFxPlhC8E/">Interactive theorem proving : 5th International Conference, ITP 2014, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 1417, 2014 : proceedings, Gerwin Klein, Ruben Gamboa (Eds.)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.bu.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.bu.edu/">Boston University 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 Interactive theorem proving : 5th International Conference, ITP 2014, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 1417, 2014 : proceedings, Gerwin Klein, Ruben Gamboa (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.bu.edu/portal/Interactivetheoremproving5thInternational/mzrFxPlhC8E/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.bu.edu/portal/Interactivetheoremproving5thInternational/mzrFxPlhC8E/">Interactive theorem proving : 5th International Conference, ITP 2014, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 1417, 2014 : proceedings, Gerwin Klein, Ruben Gamboa (Eds.)</a></span>  <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.bu.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.bu.edu/">Boston University Libraries</a></span></span></span></span></div>