6. HUG 1993:
Vancouver, BC, Canada
Jeffrey J. Joyce, Carl-Johan H. Seger (Eds.):
Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings.
Lecture Notes in Computer Science 780 Springer 1994, ISBN 3-540-57826-9 
- Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson:
Program Verification using HOL-UNITY.
1-15
- Kim Dam Petersen:
Graph model of LAMBDA in Higher Order Logic.
16-28
- Cui Zhang, Robert J. Shaw, Ronald A. Olsson, Karl N. Levitt, Myla Archer, Mark Heckman, Gregory D. Benson:
Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOL.
29-42
- Don Syme:
Reasoning with the Formal Definition of Standard ML in HOL.
43-60
- Myra Van Inwegen, Elsa L. Gunter:
HOL-ML.
61-74
- Kees G. W. Goossens:
Stucture and Behaviour in Hardware Verification.
75-88
- Catia M. Angelo, Luc J. M. Claesen, Hugo De Man:
Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL.
89-100
- Dirk Eisenbiegler, Klaus Schneider, Ramayya Kumar:
A Functional Approach for Formalizing Regular Hardware Structures.
101-114
- Laurent Théry:
A Proof Development System for HOL.
115-128
- Rachel E. O. Roxas:
A HOL Package for Reasoning about Relations Defined by Mutual Induction.
129-140
- Elsa L. Gunter:
A Broader Class of Trees for Recursive Type Definitions for HOL.
141-154
- David Lorge Parnas:
Some Theorems We Should Prove.
155-162
- John M. Rushby, Mandayam K. Srivas:
Using PVS to Prove Some Theorems Of David Parnas.
163-173
- John Harrison, Laurent Théry:
Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals.
174-184
- Jeffrey J. Joyce, Carl-Johan H. Seger:
The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover.
185-198
- Juin-Yeu Lu, Shiu-Kai Chin:
Linking HOL to a VLSI CAD System.
199-212
- Klaus Schneider, Ramayya Kumar, Thomas Kropf:
Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic.
213-226
- Anthony McIsaac:
A Formalization of Abstraction in LAMBDA.
227-238
- Tej Arora, Tony Leung, Karl N. Levitt, E. Thomas Schubert, Phillip J. Windley:
Report on the UCD Microcoded Viper Verification Project.
239-252
- Zheng Zhu, Jeffrey J. Joyce, Carl-Johan H. Seger:
Verification of the Tamarack-3 Microprocessor in a Hybrid Verification Environment.
253-266
- David A. Fura, Phillip J. Windley, Arun K. Somani:
Abstraction Techniques for Modeling Real-World Interface Chips.
267-280
- Sofiène Tahar, Ramayya Kumar:
Implementing a Methodology for Formally Verifying RISC Processors in HOL.
281-294
- Sten Agerholm:
Domain Theory in HOL.
295-309
- Ching-Tsun Chou:
Predicates, Temporal Logic, and Simulations.
310-323
- I. S. W. B. Prasetya:
Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties.
324-337
- Nancy A. Day, Jeffrey J. Joyce:
The Semantics of Statecharts in HOL.
338-351
- Monica Nesi:
Value-Passing CCS in HOL.
352-365
- Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi:
TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory.
366-370
- Wai Wong:
Modelling Bit Vectors in HOL: the word library.
371-384
- Klaus Schneider, Ramayya Kumar, Thomas Kropf:
Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification.
385-398
- Mark Aagaard, Miriam Leeser, Phillip J. Windley:
Toward a Super Duper Hardware Tactic.
399-412
- Andrew D. Gordon:
A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion.
413-425
- John Harrison:
A HOL Decision Procedure for Elementary Real Algebra.
426-435
- Konrad Slind:
AC Unification in HOL90.
436-449
- Stephen H. Brackin, Shiu-Kai Chin:
Server-Process Restrictiveness in HOL.
450-463
- Matthew J. Morley:
Safety in Railway Signalling Data: A Behavioural Analysis.
464-474
- I. S. W. B. Prasetya:
On the Style of Mechanical Proving.
475-488
- Sreeranga P. Rajan, Jeffrey J. Joyce, Carl-Johan H. Seger:
From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation.
489-500
- Victor Carreño:
Verification in Higher Order Logic of Mutual Exclusion Algorithm.
501-513
- Sara Kalvala:
Using Isabelle to Prove Simple Theorems.
514-517
Last update Mon May 20 16:04:04 2013
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
