4. TPHOLs 1991:
Davis,
CA,
USA
Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, Phillip J. Windley (Eds.):
Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, August 1991, Davis, California, USA.
IEEE Computer Society 1992 BibTeX
@proceedings{DBLP:conf/tphol/1991,
editor = {Myla Archer and
Jeffrey J. Joyce and
Karl N. Levitt and
Phillip J. Windley},
title = {Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, August 1991, Davis, California,
USA},
booktitle = {TPHOLs},
publisher = {IEEE Computer Society},
year = {1992},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
Tutorial Papers
Workshop Papers
- Kurt Keutzer:
The Need for Formal Verification in Hardware Design and What Formal Verification Has Not Done for Me Lately.
77-86 BibTeX
- E. Thomas Schubert:
Verification of Composed Hardware Systems Using CCS.
88-95 BibTeX
- J. W. Gambles, Phillip J. Windley:
An HOL Theory for Logic States with Indeterminate Strengths.
96-103 BibTeX
- X. Wang, Edward P. Stabler:
Formalization of VHDL Synthesis Procedure in Higher-Order Logic.
106-120 BibTeX
- Shiu-Kai Chin, Graham M. Birtwistle:
Implementing and Verifying Finite-State Machines Using Types in Higher-Order Logic.
121-129 BibTeX
- Simon Bainbridge, Albert John Camilleri, Roger Fleming:
Industrial Application of Theorem Proving to System Level Design.
130-142 BibTeX
- Richard Gerber, Elsa L. Gunter, Insup Lee:
Implementing a Real-Time Process Algebra in HOL.
144-154 BibTeX
- Joakim von Wright:
Mechanising the Temporal Logic of Actions in HOL.
155-159 BibTeX
- D. Shepherd:
Using HOL to produce custom verification tools.
162-169 BibTeX
- Ramayya Kumar, Thomas Kropf, Klaus Schneider:
Integrating a First-Order Automatic Prover in the HOL Environment.
170-176 BibTeX
- Jim Grundy:
Window Inference in the HOL System.
177-189 BibTeX
- Ramayya Kumar, Thomas Kropf, Klaus Schneider:
First Steps Towards Automating Hardware Proofs in HOL.
190-193 BibTeX
- John M. Rushby:
Design Choices in Specification Languages and Verification Systems.
195-204 BibTeX
- Sten Agerholm:
Mechanizing Program Verification in HOL.
208-222 BibTeX
- Rachel E. O. Roxas, Malcolm C. Newey:
Proof of Program Transformations.
223-230 BibTeX
- Joakim von Wright, Kaisa Sere:
Program Transformations and Refinements in HOL.
231-239 BibTeX
- David F. Martin, R. J. Toal:
Case Studies in Compiler Correctness Using HOL.
242-252 BibTeX
- Paul Curzon:
A Verified Compiler for a Structured Assembly Language.
253-262 BibTeX
Jim Alves-Foss,
Karl N. Levitt:
Mechanical Verification of Secure Distributed Systems in Higher Order Logic. 263-278
- R. D. Arthan:
A Report on ICL HOL.
280-283 BibTeX
- George Fink, Myla Archer, Lie Yang:
PM: A Proof Manager for HOL and Other Provers.
286-304 BibTeX
- Sara Kalvala:
Developing an Interface for HOL.
305-317 BibTeX
- Matt Kaufmann:
An Informal Discussion of Issues in Mechanically-Assisted Reasoning.
318-337 BibTeX
- Catia M. Angelo, Diederik Verkest, Luc J. M. Claesen, Hugo De Man:
Formal Hardware Verification in HOL and in Boyer-Moore: A Comparative Analysis.
340-347 BibTeX
- Thomas F. Melham:
A Package for Inductive Relation Definitions in HOL.
350-357 BibTeX
- W. Ploegaerts, Luc J. M. Claesen, Hugo De Man:
Defining Recursive Functions in HOL.
358-366 BibTeX
- Flemming Andersen, Kim Dam Petersen:
Recursive Boolean Functions in HOL.
367-377 BibTeX
- Malcolm C. Newey:
Proof Based Computation.
380-383 BibTeX
- E. de Barros Lucena:
Reasoning about Petri Nets in HOL.
384-394 BibTeX
- W. Wong:
A Simple Graph Theory and Its Application in Railway Signalling.
395-409 BibTeX
Copyright © Sat May 16 23:43:56 2009
by Michael Ley (ley@uni-trier.de)
