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

ISBN-13: 9783540578260 / Angielski / Miękka / 1994 / 526 str.

Jeffrey J. Joyce; Carl-Johan H. Seger

Opis

Containing the edited proceedings of the 1993 Higher-Order Logic User's Group Workshop, held at the University of British Columbia, Vancouver, Canada in August 1993, this volume explores higher-order logic theory proving, its usage and applications.

Spis treści

Program verification using HOL-UNITY.- Graph model of LAMBDA in higher order logic.- Mechanizing a programming logic for the concurrent programming language microSR in HOL.- Reasoning with the formal definition of standard ML in HOL.- HOL-ML.- Structure and behaviour in hardware verification.- Degrees of formality in shallow embedding hardware description languages in HOL.- A functional approach for formalizing regular hardware structures.- A proof development system for the HOL theorem prover.- A HOL package for reasoning about relations defined by mutual induction.- A broader class of trees for recursive type definitions for HOL.- Some theorems we should prove.- Using PVS to prove some theorems of David Parnas.- Extending the HOL theorem prover with a computer algebra system to reason about the reals.- The HOL-Voss system: Model-checking inside a general-purpose theorem-prover.- Linking Higher Order Logic to a VLSI CAD system.- Alternative proof procedures for finite-state machines in higher-order logic.- A formalization of abstraction in LAMBDA.- Report on the UCD microcoded Viper verification project.- Verification of the Tamarack-3 microprocessor in a hybrid verification environment.- Abstraction techniques for modeling real-world interface chips.- Implementing a methodology for formally verifying RISC processors in HOL.- Domain theory in HOL.- Predicates, temporal logic, and simulations.- Formalization of variables access constraints to support compositionality of liveness properties.- The semantics of statecharts in HOL.- Value-passing CCS in HOL.- TPS: An interactive and automatic tool for proving theorems of type theory.- Modelling bit vectors in HOL: The word library.- Eliminating higher-order quantifiers to obtain decision procedures for hardware verification.- Toward a super duper hardware tactic.- A mechanisation of name-carrying syntax up to alpha-conversion.- A HOL decision procedure for elementary real algebra.- AC unification in HOL90.- Server-process restrictiveness in HOL.- Safety in railway signalling data: A behavioural analysis.- On the style of mechanical proving.- From abstract data types to shift registers:.- Verification in higher order logic of mutual exclusion algorithm.- Using Isabelle to prove simple theorems.