Higher Order Logic Theorem Proving and Its Applications
Proceedings of the IFIP/WG10.2 International Workshop, Leuven, Belgium, 21-24 September 1992
Published on 3. February 1993
Book
Paperback/Softback
582 pages
978-0-444-89880-7 (ISBN)
Description
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.
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.
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.
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.
More details
Series
Language
English
Place of publication
Oxford
United Kingdom
Publishing group
Elsevier Science & Technology
Target group
College/higher education
Professional and scholarly
Dimensions
Height: 230 mm
ISBN-13
978-0-444-89880-7 (9780444898807)
Copyright in bibliographic data is held by Nielsen Book Services Limited or its licensors: all rights reserved.
Schweitzer Classification
Other editions
Additional editions
L. J. M. Claesen | M. J. C. Gordon
Higher Order Logic Theorem Proving and its Applications
Proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications - HOL '92 Leuven, Belgium, 21-24 September 1992
E-Book
05/2014
Elsevier
€149.00
Available for download
Content
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.