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

Program verification using HOL-UNITY....Pages 1-15
Graph model of LAMBDA in higher order logic....Pages 16-28
Mechanizing a programming logic for the concurrent programming language microSR in HOL....Pages 29-42
Reasoning with the formal definition of standard ML in HOL....Pages 43-60
HOL-ML....Pages 61-74
Structure and behaviour in hardware verification....Pages 75-88
Degrees of formality in shallow embedding hardware description languages in HOL....Pages 89-100
A functional approach for formalizing regular hardware structures....Pages 101-114
A proof development system for the HOL theorem prover....Pages 115-128
A HOL package for reasoning about relations defined by mutual induction....Pages 129-140
A broader class of trees for recursive type definitions for HOL....Pages 141-154
Some theorems we should prove....Pages 155-162
Using PVS to prove some theorems of David Parnas....Pages 163-173
Extending the HOL theorem prover with a computer algebra system to reason about the reals....Pages 174-184
The HOL-Voss system: Model-checking inside a general-purpose theorem-prover....Pages 185-198
Linking Higher Order Logic to a VLSI CAD system....Pages 199-212
Alternative proof procedures for finite-state machines in higher-order logic....Pages 213-226
A formalization of abstraction in LAMBDA....Pages 227-238
Report on the UCD microcoded Viper verification project....Pages 239-252
Verification of the Tamarack-3 microprocessor in a hybrid verification environment....Pages 253-266
Abstraction techniques for modeling real-world interface chips....Pages 267-280
Implementing a methodology for formally verifying RISC processors in HOL....Pages 281-294
Domain theory in HOL....Pages 295-309
Predicates, temporal logic, and simulations....Pages 310-323
Formalization of variables access constraints to support compositionality of liveness properties....Pages 324-337
The semantics of statecharts in HOL....Pages 338-351
Value-passing CCS in HOL....Pages 352-365
TPS: An interactive and automatic tool for proving theorems of type theory....Pages 366-370
Modelling bit vectors in HOL: The word library....Pages 371-384
Eliminating higher-order quantifiers to obtain decision procedures for hardware verification....Pages 385-398
Toward a super duper hardware tactic....Pages 399-412
A mechanisation of name-carrying syntax up to alpha-conversion....Pages 413-425
A HOL decision procedure for elementary real algebra....Pages 426-436
AC unification in HOL90....Pages 437-449
Server-process restrictiveness in HOL....Pages 450-463
Safety in railway signalling data: A behavioural analysis....Pages 464-474
On the style of mechanical proving....Pages 475-488
From abstract data types to shift registers:....Pages 489-500
Verification in higher order logic of mutual exclusion algorithm....Pages 501-513
Using Isabelle to prove simple theorems....Pages 514-517