Higher Order Logic Theorem Proving and Its Applications: 6th International Workshop, HUG '93, Vancouver, B.C., Canada, August 11-13, 1993. Proceedings

Front Cover
Jeffrey J. Joyce, Carl-Johan H. Seger
Springer Science & Business Media, Apr 28, 1994 - Computers - 526 pages
This volume constitutes the refereed proceedings of the 1993 Higher-Order Logic User's Group Workshop, held at the University of British Columbia in August 1993. The workshop was sponsored by the Centre for Integrated Computer System Research. It was the sixth in the series of annual international workshops dedicated to the topic of Higher-Order Logic theorem proving, its usage in the HOL system, and its applications. The volume contains 40 papers, including an invited paper by David Parnas, McMaster University, Canada, entitled "Some theorems we should prove".
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Program Verification using HOLUNITY
1
Graph model of LAMBDA in Higher Order Logic
16
Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOL
29
Reasoning with the Formal Definition of Standard ML in HOL
43
HOLML
61
Structure and Behaviour in Hardware Verification
75
Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL
89
A Functional Approach for Formalizing Regular Hardware Structures
101
Implementing a Methodology for Formally Verifying RISC Processors in HOL
281
Domain Theory in HOL
295
Predicates Temporal Logic and Simulations
310
Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties
324
The Semantics of Statecharts in HOL
338
ValuePassing CCS in HOL
352
An Interactive and Automatic Tool for Proving Theorems of Type Theory
366
the word Library
371

A Proof Development System for the HOL
115
A HOL Package for Reasoning about Relations Defined by Mutual Induction
129
A Broader Class of Trees for Recursive Type Definitions for HOL
141
Some Theorems We Should Prove
155
Using PVS to Prove Some Theorems of David Parnas
163
Extending the HOL Theorem Prover with a Computer Algebra System to Reason About the Reals
174
ModelChecking inside a GeneralPurpose TheoremProver
185
Linking Higher Order Logic to a VLSI CAD System
199
Alternative Proof Procedures for FiniteState Machines in HigherOrder Logic
213
A Formalization of Abstraction in LAMBDA
227
Report on the UCD Microcoded Viper Verification Project
239
Verification of the Tamarack3 Microprocessor in A Hybrid Verification Environment
253
Abstraction Techniques for Modeling RealWorld Interface Chips
267
Eliminating HigherOrder Quantifiers to Obtain Decision Procedures for Hardware Verification
385
Toward a Super Duper Hardware Tactic
399
A Mechanisation of Namecarrying Syntax up to AlphaConversion
413
A HOL Decision Procedure for Elementary Real Algebra
426
AC Unification in HOL90
437
ServerProcess Restrictiveness in HOL
450
A Behavioural Analysis
464
On the Style of Mechanical Proving
475
A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation
489
Verification in Higher Order Logic of Mutual Exclusion Algorithm
501
Using Isabelle to Prove Simple Theorems
514
Author Index
518
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information