Higher Order Logic Theorem Proving and Its Applications
Home > Computing and Information Technology > Computer science > Mathematical theory of computation > Higher Order Logic Theorem Proving and Its Applications: Proceedings of the IFIP/WG10.2 International Workshop, Leuven, Belgium, 21-24 September 1992(v. A-20 IFIP Transactions A: Computer Science and Technology)
Higher Order Logic Theorem Proving and Its Applications: Proceedings of the IFIP/WG10.2 International Workshop, Leuven, Belgium, 21-24 September 1992(v. A-20 IFIP Transactions A: Computer Science and Technology)

Higher Order Logic Theorem Proving and Its Applications: Proceedings of the IFIP/WG10.2 International Workshop, Leuven, Belgium, 21-24 September 1992(v. A-20 IFIP Transactions A: Computer Science and Technology)


     0     
5
4
3
2
1



Out of Stock


Notify me when this book is in stock
X
About the Book

The HOL system is a higher order logic theorem proving system implemented at Edinburgh University, Cambridge University and INRIA. Its applications, from the verification of hardware designs at all levels to the verification of programs and communication protocols, are considered in depth in this volume. Other systems based on higher order logic, namely Nuprl and LAMBDA are also discussed. Features given particular consideration are: novel developments in higher order logic and its implementations in HOL; formal design and verification methodologies for hardware and software; and public domain availability of the HOL system. Papers addressing these issues have been divided as follows: mathematical logic; induction; general modelling and proofs; formalizing and modelling of automata; program verification; hardware description language semantics; hardware verification methodologies; simulation in higher order logic; and extended uses of higher order logic. Academic and industrial researchers involved in formal hardware and software design and verification methods should find the publication especially interesting, and it is hoped it will also provide a useful reference tool for those working at software institutes and within the electronics industries.

Table of Contents:
Part 1 Mathematical logic: the HOL logic extended with quantification over type variables, T.F. Melham; a lazy approach to fully-expansive theorem proving, R.J. Boulton; efficient representation and computation of tableaux proofs, K. Schneider et al; a note on interactive theorem proving with theorem continuation functions, C.-T. Chou; a sequent formulation of a logic of predicates in HOL, C.-T. Chou; a classical type theory with transfinite types, G. Pottinger. Part 2 Induction: unification-based induction, H. Busch; introducing well-founded function definitions in HOL, M. van der Voort; Boyer-Moore automation for the HOL system, R.J. Boulton. Part 3 General modelling and proofs: constructing the real numbers in HOL, J. Harrison; modelling generic hardware structures by abstract datatypes, K. Schneider et al; a methodology for reusable hardware proofs, M. Aagaard and M. Leeser; abstract theories in HOL, P.J. Windley; machine abstraction in microprocessor specification, M. McAllister. Part 4 Formalizing and modelling of automata: a formal theory of simulations between infinite automata, P. Loewenstein; a comparison between statecharts and state transition assertions, N. Day; an embedding of timed transition systems in HOL, R. Cardell-Oliver et al; formalizing a modal logic for CSS in the HOL theorem prover, M. Nesi; modelling non-deterministic systems in HOL, J. Alves-Foss. Part 5 Program verification: mechanizing some advanced refinement concepts, J. von Wright et al; deriving correctness properties of compiled code, P. Curzon; a HOL mechanization of the axiomatic semantics of a simple distributed programming language, W.L. Harrison et al. Part 6 Hardware description language semantics: a formalization of the VHDL simulation cycle, J.P. van Tassel; the formal semantics definition of a multi-rate DSP specification language in HOL, C. Angelo et al; design-flow graph partitioning, R.B. Hughes and G. Musgrave. Part 7 Hardware verification methodologies: implementation and use of annotations in HOL, S. Kalvala et al; towards a formal verification of a floating point coprocessor and its composition with a central processing unit, J. Pan et al; deriving a correct computer, L.-G. Wang; formal tools for tri-state design in busses, R.B. Hughes et al; specification and formal synthesis of digital circuits, M. Bombana et al. Part 8 Simulation in higher order logic: operational semantics based formal symbolic simulation, K.G.W. Goosens; simulating microprocessors from formal specifications, K.M. Hall and P.J. Windley; executing HOL specifications - towards an evaluation semantics for classical higher order logic, P.S. Rajan. Part 9 Extended uses of higher order logic: linking other theorem provers to HOL using PM - proof manager, M. Archer et al; adding new rules to an LCF-style logic implementation, K. Slind; why we can't have SML style declarations in HOL, E.L. Gunter.


Best Sellers


Product Details
  • ISBN-13: 9780444898807
  • Publisher: Elsevier Science & Technology
  • Publisher Imprint: Elsevier Science Ltd
  • Height: 230 mm
  • Sub Title: Proceedings of the IFIP/WG10.2 International Workshop, Leuven, Belgium, 21-24 September 1992
  • ISBN-10: 0444898808
  • Publisher Date: 03 Feb 1993
  • Binding: Paperback
  • Series Title: v. A-20 IFIP Transactions A: Computer Science and Technology


Similar Products

Add Photo
Add Photo

Customer Reviews

REVIEWS      0     
Click Here To Be The First to Review this Product
Higher Order Logic Theorem Proving and Its Applications: Proceedings of the IFIP/WG10.2 International Workshop, Leuven, Belgium, 21-24 September 1992(v. A-20 IFIP Transactions A: Computer Science and Technology)
Elsevier Science & Technology -
Higher Order Logic Theorem Proving and Its Applications: Proceedings of the IFIP/WG10.2 International Workshop, Leuven, Belgium, 21-24 September 1992(v. A-20 IFIP Transactions A: Computer Science and Technology)
Writing guidlines
We want to publish your review, so please:
  • keep your review on the product. Review's that defame author's character will be rejected.
  • Keep your review focused on the product.
  • Avoid writing about customer service. contact us instead if you have issue requiring immediate attention.
  • Refrain from mentioning competitors or the specific price you paid for the product.
  • Do not include any personally identifiable information, such as full names.

Higher Order Logic Theorem Proving and Its Applications: Proceedings of the IFIP/WG10.2 International Workshop, Leuven, Belgium, 21-24 September 1992(v. A-20 IFIP Transactions A: Computer Science and Technology)

Required fields are marked with *

Review Title*
Review
    Add Photo Add up to 6 photos
    Would you recommend this product to a friend?
    Tag this Book Read more
    Does your review contain spoilers?
    What type of reader best describes you?
    I agree to the terms & conditions
    You may receive emails regarding this submission. Any emails will include the ability to opt-out of future communications.

    CUSTOMER RATINGS AND REVIEWS AND QUESTIONS AND ANSWERS TERMS OF USE

    These Terms of Use govern your conduct associated with the Customer Ratings and Reviews and/or Questions and Answers service offered by Bookswagon (the "CRR Service").


    By submitting any content to Bookswagon, you guarantee that:
    • You are the sole author and owner of the intellectual property rights in the content;
    • All "moral rights" that you may have in such content have been voluntarily waived by you;
    • All content that you post is accurate;
    • You are at least 13 years old;
    • Use of the content you supply does not violate these Terms of Use and will not cause injury to any person or entity.
    You further agree that you may not submit any content:
    • That is known by you to be false, inaccurate or misleading;
    • That infringes any third party's copyright, patent, trademark, trade secret or other proprietary rights or rights of publicity or privacy;
    • That violates any law, statute, ordinance or regulation (including, but not limited to, those governing, consumer protection, unfair competition, anti-discrimination or false advertising);
    • That is, or may reasonably be considered to be, defamatory, libelous, hateful, racially or religiously biased or offensive, unlawfully threatening or unlawfully harassing to any individual, partnership or corporation;
    • For which you were compensated or granted any consideration by any unapproved third party;
    • That includes any information that references other websites, addresses, email addresses, contact information or phone numbers;
    • That contains any computer viruses, worms or other potentially damaging computer programs or files.
    You agree to indemnify and hold Bookswagon (and its officers, directors, agents, subsidiaries, joint ventures, employees and third-party service providers, including but not limited to Bazaarvoice, Inc.), harmless from all claims, demands, and damages (actual and consequential) of every kind and nature, known and unknown including reasonable attorneys' fees, arising out of a breach of your representations and warranties set forth above, or your violation of any law or the rights of a third party.


    For any content that you submit, you grant Bookswagon a perpetual, irrevocable, royalty-free, transferable right and license to use, copy, modify, delete in its entirety, adapt, publish, translate, create derivative works from and/or sell, transfer, and/or distribute such content and/or incorporate such content into any form, medium or technology throughout the world without compensation to you. Additionally,  Bookswagon may transfer or share any personal information that you submit with its third-party service providers, including but not limited to Bazaarvoice, Inc. in accordance with  Privacy Policy


    All content that you submit may be used at Bookswagon's sole discretion. Bookswagon reserves the right to change, condense, withhold publication, remove or delete any content on Bookswagon's website that Bookswagon deems, in its sole discretion, to violate the content guidelines or any other provision of these Terms of Use.  Bookswagon does not guarantee that you will have any recourse through Bookswagon to edit or delete any content you have submitted. Ratings and written comments are generally posted within two to four business days. However, Bookswagon reserves the right to remove or to refuse to post any submission to the extent authorized by law. You acknowledge that you, not Bookswagon, are responsible for the contents of your submission. None of the content that you submit shall be subject to any obligation of confidence on the part of Bookswagon, its agents, subsidiaries, affiliates, partners or third party service providers (including but not limited to Bazaarvoice, Inc.)and their respective directors, officers and employees.

    Accept

    New Arrivals


    Inspired by your browsing history


    Your review has been submitted!

    You've already reviewed this product!