## Higher Order Logic Theorem Proving and Its Applications: 6th International Workshop, HUG '93, Vancouver, B.C., Canada, August 11-13, 1993. ProceedingsJeffrey J. Joyce, Carl-Johan H. Seger 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 |

518 | |

### Other editions - View all

### Common terms and phrases

abstraction algorithm applied approach assertions automated automatically behaviour bool boolean buffered circuits component Computer Science construction constructors correctness corresponding data type defined definition denotes derived described domain embedding equations evaluation example expressions finite formal formal verification formulae FSM-goals function given goal hardware description languages hardware verification Higher Order Logic higher-order logic Hoare logic HOL theorem prover HOL-Voss implementation induction inference rules input instantiation instruction interpreter invocval pname label LAMBDA lemma lift Melham microprocessor microSR natural numbers Nuprl operation operational semantics output paper parameters predicate proof system properties prove pure CCS PWORDLEN quantified recursive type relation represented result rewriting satisfies semantics signals Silage simulation specification Standard ML step structural subgoals subset subtrees symbolic syntax tactic Technical Report temporal theorem prover theory tion transition translation University University of Cambridge value-passing variables Viper