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".
Author(s): Flemming Andersen, Kim Dam Petersen (auth.), Jeffrey J. Joyce, Carl-Johan H. Seger (eds.)
Series: Lecture Notes in Computer Science 780
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1994
Language: English
Pages: 526
Tags: Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics); Software Engineering; Arithmetic and Logic Structures; Logic Design
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
