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 / organized by CHEOPS ESPRIT BRA 3215 ; sponsored by IMEC and the Commission of the European Communities, Leuven, Belgium, 21-24 September 1992 ; edited by Luc J.M. Claesen, Michael J.C. Gordon
- Conference Author
- IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and Its Applications (1992 : Louvain, Belgium)
- Published
- Amsterdam ; New York : North-Holland, 1993.
- Physical Description
- 1 online resource (xiii, 568 pages) : illustrations
- Additional Creators
- Claesen, Luc J. M., Gordon, Michael J. C., 1948-, Interuniversity Micro-Electronics Center, and Commission of the European Communities
Access Online
- Series
- Contents
- Machine generated contents note: Ch. 1 Mathematical Logic Issues -- "The HOL Logic Extended with Quantification over Type Variables" / Thomas F. Melham -- "A Lazy Approach to Fully-Expansive Theorem Proving" / Richard Boulton -- "Efficient Representation and Computation of Tableaux Proofs" / Klaus Schneider / Ramayya Kumar / Thomas Kropf -- "A Note on Interactive Theorem Proving with Theorem Continuation Functions" / Ching-Tsun Chou -- "A Sequent Formulation of a Logic of Predicates in HOL" / Ching-Tsun Chou -- "A Classical Type Theory with Transfinite Types" / Garrel Pottinger -- Ch. 2 Induction -- "Unification-Based Induction" / Holger Busch -- "Introducing well-founded function definitions in HOL" / Mark van der Voort -- "Boyer-Moore Automation for the HOL System" / Richard J. Boulton -- Ch. 3 General Modelling and Proofs -- "Constructing the real numbers in HOL" / John Harrison -- "Modelling Generic Hardware Structures by Abstract Datatypes" / Ramayya Kumar / Thomas Kropf / Klaus Schneider -- "A Methodology for Reusable Hardware Proofs" / Mark Aagaard / Miriam Leeser -- "Abstract Theories in HOL" / Phillip J. Windley -- "Machine Abstraction in Microprocessor Specification" / Michael McAllister -- Ch. 4 Formalizing and Modelling of Automata -- "A Formal Theory of Simulations Between Infinite Automata" / Paul Loewenstein -- "A Comparison between Statecharts and State Transition Assertions" / Nancy Day -- "An Embedding of Timed Transition Systems in HOL" / Rachel Cardell-Oliver / Roger Hale / John Herbert -- "Formalizing a Modal Logic for CSS in the HOL Theorem Prover" / Monica Nesi -- "Modelling Non-Deterministic Systems in HOL" / Jim Alves-Foss -- Ch. 5 Program Verification -- "Mechanising some Advanced Refinement Concepts" / Joakim von Wright / J. Hekanaho / P. Luostarinen / T. Langbacka -- "Deriving Correctness Properties of Compiled Code" / Paul Curzon -- "A HOL Mechanization of The Axiomatic Semantics of a Simple Distributed Programming Language" / William L. Harrison / Karl N. Levitt / Myla M. Archer -- Ch. 6 Hardware Description Language Semantics -- "A Formalisation of the VHDL Simulation Cycle" / John P. Van Tassel -- "The Formal Semantics Definition of a Multi-Rate DSP Specification Language in HOL" / C. Angelo / L. Claesen / H. De Man -- "Design-Flow Graph Partitioning" / R. B. Hughes / G. Musgrave -- Ch. 7 Hardware Verification Methodologies -- "Implementation and Use of Annotations in HOL" / Karl Levitt / Myla Archer / Saraswati Kalvala -- "Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit" / Sara Kalvala / Myla Archer / Karl N. Levitt / Jing Pan -- "Deriving a Correct Computer" / Li-Guo Wang -- "Formal Tools for Tri-State Design in Busses" / S. P. Finn / M. D. Francis / R. B. Hughes / G. Musgrave -- "Specification and Formal Synthesis of Digital Circuits" / P. Cavalloro / G. Zaza / M. Bombana -- Ch. 8 Simulation in Higher Order Logic -- "Operational Semantics Based Formal Symbolic Simulation" / K. G. W. Goossens -- "Simulating Microprocessors from Formal Specifications" / Phillip J. Windley / Kelly M. Hall -- "Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic" / P. Sreeranga Rajan -- Ch. 9 Extended uses of Higher Order Logic -- "Linking Other Theorem Provers to HOL Using PM: Proof Manager" / Myla Archer / Lie Yang / George Fink -- "Adding New Rules to an LCF-style Logic Implementation" / Konrad Slind.
- Summary
- The HOL system is a higher order logic theorem proving system implemented at Edinburgh University, Cambridge University and INRIA. Its many 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; 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; 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.
- Subject(s)
- Automatic theorem proving—Congresses
- Logic, Symbolic and mathematical—Congresses
- COMPUTERS—Computer Literacy
- COMPUTERS—Computer Science
- COMPUTERS—Data Processing
- COMPUTERS—Hardware—General
- COMPUTERS—Information Technology
- COMPUTERS—Machine Theory
- COMPUTERS—Reference
- Automatic theorem proving
- Logic, Symbolic and mathematical
- Programmatuurtechniek
- Logica
- Bewijstheorie
- Théorèmes—Démonstration automatique—Congrès
- Logique symbolique et mathématique—Congrès
- Induction (logique)—Congrès
- Genre(s)
- ISBN
- 0444898808 (electronic bk.)
9780444898807 (electronic bk.)
9781483298405
148329840X - Bibliography Note
- Includes bibliographical references.
View MARC record | catkey: 18157666