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 Higher Order Logic Theorem Proving and Its Applications : 8th International Workshop Aspen Grove, UT, USA, September 11–14, 1995 Proceedings, edited by E. Thomas Schubert, Philip J. Windley, James AlvesFoss, (electronic resource)
Higher Order Logic Theorem Proving and Its Applications : 8th International Workshop Aspen Grove, UT, USA, September 11–14, 1995 Proceedings, edited by E. Thomas Schubert, Philip J. Windley, James AlvesFoss, (electronic resource)
Resource Information
The item Higher Order Logic Theorem Proving and Its Applications : 8th International Workshop Aspen Grove, UT, USA, September 11–14, 1995 Proceedings, edited by E. Thomas Schubert, Philip J. Windley, James AlvesFoss, (electronic resource) 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 Higher Order Logic Theorem Proving and Its Applications : 8th International Workshop Aspen Grove, UT, USA, September 11–14, 1995 Proceedings, edited by E. Thomas Schubert, Philip J. Windley, James AlvesFoss, (electronic resource) 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 8th International Conference on Higher Order Logic Theorem Proving and Its Applications, held in Aspen Grove, Utah, USA in September 1995. The 26 papers selected by the program committee for inclusion in this volume document the advances in the field achieved since the predecessor conference. The papers presented fall into three general categories: representation of formalisms in higher order logic; applications of mechanized higher order logic; and enhancements to the HOL and other theorem proving systems
 Language
 eng
 Extent
 VIII, 408 p.
 Contents

 Mechanizing a ?calculus equivalence in HOL
 Nonprimitive recursive function definitions
 Experiments with ZF set theory in HOL and Isabelle
 Automatically synthesized term denotation predicates: A proof aid
 On the refinement of symmetric memory protocols
 Combining decision procedures in the HOL system
 Deciding cryptographic protocol adequacy with HOL
 A practical method for reasoning about distributed systems in a theorem prover
 A theory of finite maps
 Virtual theories
 An automata theory dedicated towards formal circuit synthesis
 Interfacing HOL90 with a functional database query language
 Floating point verification in HOL
 Inductive definitions: Automation and application
 A formulation of TLA in Isabelle
 Formal verification of serial pipeline multipliers
 TkWinHOL: A tool for Window Inference in HOL
 Formal verification of counterflow pipeline architecture
 Deep embedding VHDL
 HOLCF: Higher order logic of computable functions
 A mechanized logic for secure key escrow protocol verification
 A new interface for HOL — Ideas, issues and implementation
 Very efficient conversions
 Recording and checking HOL proofs
 Formalization of planar graphs
 A hierarchical method for reasoning about distributed programming languages
 Isbn
 9783540447849
 Label
 Higher Order Logic Theorem Proving and Its Applications : 8th International Workshop Aspen Grove, UT, USA, September 11–14, 1995 Proceedings
 Title
 Higher Order Logic Theorem Proving and Its Applications
 Title remainder
 8th International Workshop Aspen Grove, UT, USA, September 11–14, 1995 Proceedings
 Statement of responsibility
 edited by E. Thomas Schubert, Philip J. Windley, James AlvesFoss
 Subject

 Artificial intelligence
 Computer Science
 Computer science
 Electronic resources
 Electronics
 Electronics and Microelectronics, Instrumentation
 Logic Design
 Logic design
 Mathematical Logic and Formal Languages
 Operating Systems
 Operating systems (Computers)
 Software Engineering
 Software engineering
 Artificial Intelligence (incl. Robotics)
 Language
 eng
 Summary
 This book constitutes the proceedings of the 8th International Conference on Higher Order Logic Theorem Proving and Its Applications, held in Aspen Grove, Utah, USA in September 1995. The 26 papers selected by the program committee for inclusion in this volume document the advances in the field achieved since the predecessor conference. The papers presented fall into three general categories: representation of formalisms in higher order logic; applications of mechanized higher order logic; and enhancements to the HOL and other theorem proving systems
 http://library.link/vocab/creatorName
 Thomas Schubert, E
 Image bit depth
 0
 LC call number
 QA8.9QA10.3
 Literary form
 non fiction
 http://library.link/vocab/relatedWorkOrContributorName

 Windley, Philip J.
 AlvesFoss, James.
 SpringerLink
 Series statement
 Lecture Notes in Computer Science,
 Series volume
 971
 http://library.link/vocab/subjectName

 Computer science
 Logic design
 Software engineering
 Operating systems (Computers)
 Artificial intelligence
 Electronics
 Computer Science
 Mathematical Logic and Formal Languages
 Artificial Intelligence (incl. Robotics)
 Logic Design
 Electronics and Microelectronics, Instrumentation
 Software Engineering
 Operating Systems
 Label
 Higher Order Logic Theorem Proving and Its Applications : 8th International Workshop Aspen Grove, UT, USA, September 11–14, 1995 Proceedings, edited by E. Thomas Schubert, Philip J. Windley, James AlvesFoss, (electronic resource)
 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
 Mechanizing a ?calculus equivalence in HOL  Nonprimitive recursive function definitions  Experiments with ZF set theory in HOL and Isabelle  Automatically synthesized term denotation predicates: A proof aid  On the refinement of symmetric memory protocols  Combining decision procedures in the HOL system  Deciding cryptographic protocol adequacy with HOL  A practical method for reasoning about distributed systems in a theorem prover  A theory of finite maps  Virtual theories  An automata theory dedicated towards formal circuit synthesis  Interfacing HOL90 with a functional database query language  Floating point verification in HOL  Inductive definitions: Automation and application  A formulation of TLA in Isabelle  Formal verification of serial pipeline multipliers  TkWinHOL: A tool for Window Inference in HOL  Formal verification of counterflow pipeline architecture  Deep embedding VHDL  HOLCF: Higher order logic of computable functions  A mechanized logic for secure key escrow protocol verification  A new interface for HOL — Ideas, issues and implementation  Very efficient conversions  Recording and checking HOL proofs  Formalization of planar graphs  A hierarchical method for reasoning about distributed programming languages
 Dimensions
 unknown
 Extent
 VIII, 408 p.
 File format
 multiple file formats
 Form of item
 electronic
 Isbn
 9783540447849
 Level of compression
 uncompressed
 Media category
 computer
 Media MARC source
 rdamedia
 Media type code

 c
 Other control number
 10.1007/3540602755
 Other physical details
 online resource.
 Quality assurance targets
 absent
 Reformatting quality
 access
 Specific material designation
 remote
 System control number
 (DEHe213)9783540447849
 Label
 Higher Order Logic Theorem Proving and Its Applications : 8th International Workshop Aspen Grove, UT, USA, September 11–14, 1995 Proceedings, edited by E. Thomas Schubert, Philip J. Windley, James AlvesFoss, (electronic resource)
 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
 Mechanizing a ?calculus equivalence in HOL  Nonprimitive recursive function definitions  Experiments with ZF set theory in HOL and Isabelle  Automatically synthesized term denotation predicates: A proof aid  On the refinement of symmetric memory protocols  Combining decision procedures in the HOL system  Deciding cryptographic protocol adequacy with HOL  A practical method for reasoning about distributed systems in a theorem prover  A theory of finite maps  Virtual theories  An automata theory dedicated towards formal circuit synthesis  Interfacing HOL90 with a functional database query language  Floating point verification in HOL  Inductive definitions: Automation and application  A formulation of TLA in Isabelle  Formal verification of serial pipeline multipliers  TkWinHOL: A tool for Window Inference in HOL  Formal verification of counterflow pipeline architecture  Deep embedding VHDL  HOLCF: Higher order logic of computable functions  A mechanized logic for secure key escrow protocol verification  A new interface for HOL — Ideas, issues and implementation  Very efficient conversions  Recording and checking HOL proofs  Formalization of planar graphs  A hierarchical method for reasoning about distributed programming languages
 Dimensions
 unknown
 Extent
 VIII, 408 p.
 File format
 multiple file formats
 Form of item
 electronic
 Isbn
 9783540447849
 Level of compression
 uncompressed
 Media category
 computer
 Media MARC source
 rdamedia
 Media type code

 c
 Other control number
 10.1007/3540602755
 Other physical details
 online resource.
 Quality assurance targets
 absent
 Reformatting quality
 access
 Specific material designation
 remote
 System control number
 (DEHe213)9783540447849
Subject
 Artificial intelligence
 Computer Science
 Computer science
 Electronic resources
 Electronics
 Electronics and Microelectronics, Instrumentation
 Logic Design
 Logic design
 Mathematical Logic and Formal Languages
 Operating Systems
 Operating systems (Computers)
 Software Engineering
 Software engineering
 Artificial Intelligence (incl. Robotics)
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/HigherOrderLogicTheoremProvingandIts/c6ng_6uBFA/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.bu.edu/portal/HigherOrderLogicTheoremProvingandIts/c6ng_6uBFA/">Higher Order Logic Theorem Proving and Its Applications : 8th International Workshop Aspen Grove, UT, USA, September 11–14, 1995 Proceedings, edited by E. Thomas Schubert, Philip J. Windley, James AlvesFoss, (electronic resource)</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 Higher Order Logic Theorem Proving and Its Applications : 8th International Workshop Aspen Grove, UT, USA, September 11–14, 1995 Proceedings, edited by E. Thomas Schubert, Philip J. Windley, James AlvesFoss, (electronic resource)
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/HigherOrderLogicTheoremProvingandIts/c6ng_6uBFA/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.bu.edu/portal/HigherOrderLogicTheoremProvingandIts/c6ng_6uBFA/">Higher Order Logic Theorem Proving and Its Applications : 8th International Workshop Aspen Grove, UT, USA, September 11–14, 1995 Proceedings, edited by E. Thomas Schubert, Philip J. Windley, James AlvesFoss, (electronic resource)</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>