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 BibTeX
@proceedings{DBLP:conf/tphol/1993,
editor = {Jeffrey J. Joyce and
Carl-Johan H. Seger},
title = {Higher Order Logic Theorem Proving and its Applications, 6th
International Workshop, HUG '93, Vancouver, BC, Canada, August
11-13, 1993, Proceedings},
booktitle = {HUG},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {780},
year = {1994},
isbn = {3-540-57826-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
- Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson:
Program Verification using HOL-UNITY.
1-15 BibTeX
- Kim Dam Petersen:
Graph model of LAMBDA in Higher Order Logic.
16-28 BibTeX
- 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 BibTeX
- Don Syme:
Reasoning with the Formal Definition of Standard ML in HOL.
43-60 BibTeX
- Myra Van Inwegen, Elsa L. Gunter:
HOL-ML.
61-74 BibTeX
- Kees G. W. Goossens:
Stucture and Behaviour in Hardware Verification.
75-88 BibTeX
- Catia M. Angelo, Luc J. M. Claesen, Hugo De Man:
Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL.
89-100 BibTeX
- Dirk Eisenbiegler, Klaus Schneider, Ramayya Kumar:
A Functional Approach for Formalizing Regular Hardware Structures.
101-114 BibTeX
- Laurent Théry:
A Proof Development System for HOL.
115-128 BibTeX
- Rachel E. O. Roxas:
A HOL Package for Reasoning about Relations Defined by Mutual Induction.
129-140 BibTeX
- Elsa L. Gunter:
A Broader Class of Trees for Recursive Type Definitions for HOL.
141-154 BibTeX
- David Lorge Parnas:
Some Theorems We Should Prove.
155-162 BibTeX
- John M. Rushby, Mandayam K. Srivas:
Using PVS to Prove Some Theorems Of David Parnas.
163-173 BibTeX
- John Harrison, Laurent Théry:
Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals.
174-184 BibTeX
- Jeffrey J. Joyce, Carl-Johan H. Seger:
The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover.
185-198 BibTeX
- Juin-Yeu Lu, Shiu-Kai Chin:
Linking HOL to a VLSI CAD System.
199-212 BibTeX
- Klaus Schneider, Ramayya Kumar, Thomas Kropf:
Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic.
213-226 BibTeX
- Anthony McIsaac:
A Formalization of Abstraction in LAMBDA.
227-238 BibTeX
- Tej Arora, Tony Leung, Karl N. Levitt, E. Thomas Schubert, Phillip J. Windley:
Report on the UCD Microcoded Viper Verification Project.
239-252 BibTeX
- Zheng Zhu, Jeffrey J. Joyce, Carl-Johan H. Seger:
Verification of the Tamarack-3 Microprocessor in a Hybrid Verification Environment.
253-266 BibTeX
- David A. Fura, Phillip J. Windley, Arun K. Somani:
Abstraction Techniques for Modeling Real-World Interface Chips.
267-280 BibTeX
- Sofiène Tahar, Ramayya Kumar:
Implementing a Methodology for Formally Verifying RISC Processors in HOL.
281-294 BibTeX
- Sten Agerholm:
Domain Theory in HOL.
295-309 BibTeX
- Ching-Tsun Chou:
Predicates, Temporal Logic, and Simulations.
310-323 BibTeX
- I. S. W. B. Prasetya:
Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties.
324-337 BibTeX
- Nancy A. Day, Jeffrey J. Joyce:
The Semantics of Statecharts in HOL.
338-351 BibTeX
- Monica Nesi:
Value-Passing CCS in HOL.
352-365 BibTeX
- 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 BibTeX
- Wai Wong:
Modelling Bit Vectors in HOL: the word library.
371-384 BibTeX
- Klaus Schneider, Ramayya Kumar, Thomas Kropf:
Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification.
385-398 BibTeX
- Mark Aagaard, Miriam Leeser, Phillip J. Windley:
Toward a Super Duper Hardware Tactic.
399-412 BibTeX
- Andrew D. Gordon:
A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion.
413-425 BibTeX
- John Harrison:
A HOL Decision Procedure for Elementary Real Algebra.
426-435 BibTeX
- Konrad Slind:
AC Unification in HOL90.
436-449 BibTeX
- Stephen H. Brackin, Shiu-Kai Chin:
Server-Process Restrictiveness in HOL.
450-463 BibTeX
- Matthew J. Morley:
Safety in Railway Signalling Data: A Behavioural Analysis.
464-474 BibTeX
- I. S. W. B. Prasetya:
On the Style of Mechanical Proving.
475-488 BibTeX
- 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 BibTeX
- Victor Carreño:
Verification in Higher Order Logic of Mutual Exclusion Algorithm.
501-513 BibTeX
- Sara Kalvala:
Using Isabelle to Prove Simple Theorems.
514-517 BibTeX
Copyright © Sat May 16 23:43:56 2009
by Michael Ley (ley@uni-trier.de)
