default search action
5th TPHOLs 1992: Leuven, Belgium
- Luc J. M. Claesen, Michael J. C. Gordon:
Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992. IFIP Transactions A-20, North-Holland/Elsevier 1993, ISBN 0-444-89880-8
Mathematical Logic Issues
- Thomas F. Melham:
The HOL Logic Extended with Quantification over Type Variables. TPHOLs 1992: 3-17 - Richard J. Boulton:
A Lazy Approach to Fully-Expansive Theorem Proving. TPHOLs 1992: 19-38 - Klaus Schneider, Ramayya Kumar, Thomas Kropf:
Efficient Representation and Computation of Tableau Proofs. TPHOLs 1992: 39-57 - Ching-Tsun Chou:
A Note on Interactive Theorem Proving with Theorem Continuation Functions. TPHOLs 1992: 59-69 - Ching-Tsun Chou:
A Sequent Formulation of a Logic of Predicates in HOL. TPHOLs 1992: 71-80 - Garrel Pottinger:
A Classical Type Theory with Transfinite Types. TPHOLs 1992: 81-94
Induction
- Holger Busch:
Unification Based Induction. TPHOLs 1992: 97-116 - Mark van der Voort:
Introducing well-founded function definitions in HOL. TPHOLs 1992: 117-131 - Richard J. Boulton:
Boyer-Moore Automation for the HOL System. TPHOLs 1992: 133-142
General Modelling and Proofs
- John Harrison:
Constructing the real numbers in HOL. TPHOLs 1992: 145-164 - Klaus Schneider, Ramayya Kumar, Thomas Kropf:
Modelling Generic Hardware Structures by Abstract Datatypes. TPHOLs 1992: 165-175 - Mark D. Aagaard, Miriam Leeser:
A Methodology for Reusable Hardware Proofs. TPHOLs 1992: 177-196 - Phillip J. Windley:
Abstract Theories in HOL. TPHOLs 1992: 197-210 - Michael McAllister:
Machine Abstraction in Microprocessor Specification. TPHOLs 1992: 211-224
Formalizing and Modelling of Automata
- Paul Loewenstein:
A Formal Theory of Simulations Between Infinite Automata. TPHOLs 1992: 227-246 - Nancy A. Day:
A Comparison between Statecharts and State Transition Assertions. TPHOLs 1992: 247-262 - Rachel Cardell-Oliver, Roger Hale, John Herbert:
An Embedding of Timed Transition Systems in HOL. TPHOLs 1992: 263-278 - Monica Nesi:
Formalizing a Modal Logic for CSS in the HOL Theorem Prover. TPHOLs 1992: 279-294 - Jim Alves-Foss:
Modelling Non-Deterministic System in HOL. TPHOLs 1992: 295-304
Program Verification
- Joakim von Wright, Jukka Hekanaho, P. Luostarinen, Thomas Långbacka:
Mechanising some Advanced Refinement Concepts. TPHOLs 1992: 307-326 - Paul Curzon:
Deriving Correctness Properties of Compiled Code. TPHOLs 1992: 327-346 - William L. Harrison, Myla Archer, Karl N. Levitt:
A HOL Mechanisation of the Axiomatic Semantics of a Simple Distributed Programming Language. TPHOLs 1992: 347-356
Hardware Description Language Semantics
- John Van Tassel:
A Formalisation of the VHDL Simulation Cycle. TPHOLs 1992: 359-374 - Catia M. Angelo, Luc J. M. Claesen, Hugo De Man:
The Formal Semantics Definition of a Multi-Rate DSP Specification Language in HOL. TPHOLs 1992: 375-394 - Roger B. Hughes, Gerry Musgrave:
Design-Flow Graph Partitioning. TPHOLs 1992: 395-404
Hardware Verification Methodologies
- Saraswati Kalvala, Myla Archer, Karl N. Levitt:
Implementation and Use of Annotations in HOL. TPHOLs 1992: 407-426 - Jing Pan, Karl N. Levitt, Myla Archer, Saraswati Kalvala:
Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit. TPHOLs 1992: 427-447 - Li-Guo Wang:
Deriving a Correct Computer. TPHOLs 1992: 449-458 - Roger B. Hughes, M. D. Francis, Simon Finn, Gerry Musgrave:
Formal Tools in Tri-State Design in Busses. TPHOLs 1992: 459-475 - Massimo Bombana, Patrizia Cavalloro, Giuseppe Zaza:
Specification and Formal Synthesis of Digital Circuits. TPHOLs 1992: 475-484
Simulation in Higher Order Logic
- Kees G. W. Goossens:
Operational Semantics Based on Formal Symbolic Simulation. TPHOLs 1992: 487-506 - Kelly M. Hall, Phillip J. Windley:
Simulating Microprocessors from Formal Specifications. TPHOLs 1992: 507-525 - Sreeranga P. Rajan:
Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic. TPHOLs 1992: 527-536
Extended Uses of Higher Oredr Logic
- Myla Archer, George Fink, Lie Yang:
Linking Other Theorem Provers to HOL Using PM: Proof Manager. TPHOLs 1992: 539-548 - Konrad Slind:
Adding New Rules to an LCF-style Logic Implementation. TPHOLs 1992: 549-559 - Elsa L. Gunter:
Why we can't have SML-style datatype Declarations in HOL. TPHOLs 1992: 561-568
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-19 20:33 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: