7. TPHOLs 1994: Valletta, Malta
Thomas F. Melham, Juanito Camilleri (Eds.):
Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings.
Lecture Notes in Computer Science 859 Springer 1994, ISBN 3-540-58450-1 
- Sten Agerholm:
LCF Examples in HOL.
1-16
- Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson:
A Graphical Tool for Proving Unity Progress.
17-32
- Catia M. Angelo, Luc J. M. Claesen, Hugo De Man:
Reasoning About a Class of Linear Systems of Equations in HOL.
33-48
- Jean-Paul Bodeveix, Mamoun Filali, P. Roche:
Towards a HOL Theory and Memory.
49-64
- Stephen H. Brackin:
Providing Tractable Security Analysis in HOL.
65-80
- N. G. de Bruijn:
Highlighting the Lambda-free Fragment of Automath.
81-96
- Holger Busch:
First-Order Automation for Higher-Order-Logic Theorem Proving.
97-112
- Juanito Camilleri, Vincent Zammit:
Symbolic Animation as a Proof Tool.
113-127
- Nick Chapman, Simon Finn, Michael P. Fourman:
Datatypes in L2.
128-143
- Ching-Tsun Chou:
A Formal Theory of Undirected Graphs in Higher-Order Logic.
144-157
- Ching-Tsun Chou:
Mechanical Verification of Distributed Algorithms in Higher-Order Logic.
158-176
- Paul Curzon:
Tracking Design Changes with Formal Verification.
177-192
- Thomas Forster:
Weak Systems of Set Theory Related to HOL.
193-204
- David A. Fura, Arun K. Somani:
Interval-Semantic Component Models and the Efficient Verification of Transaction-Level Circiut Behavior.
205-220
- Brian T. Graham:
An Interpretation of NODEN in HOL.
221-234
- Keith Hanna:
Reasoning about Real Circuits.
235-253
- John Harrison:
Binary Decision Diagrams as a HOL Derived Rule.
254-268
- Peter V. Homeier, David F. Martin:
Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition Generator.
269-284
- Jeffrey J. Joyce, Nancy A. Day, Michael R. Donat:
S: A Machine Readable Specification Notation based on Higher Order Logic.
285-299
- Mats Larsson:
An Engineering Approach to Formal Digital System Design.
300-315
- Juin-Yeu Lu, Shiu-Kai Chin:
Generating Designs Using an Algorithmic Register Transfer Language with Formal Semantics.
316-331
- Thomas Långbacka:
A HOL Formalisation of the Temporal Logic of Actions.
332-345
- Savi Maharaj, Elsa L. Gunter:
Studying the ML Module System in Hol.
346-361
- I. S. W. B. Prasetya:
Towards a Mechanically Supported and Compositional Calculus to Design Destributed Algorithms.
362-377
- Ralf Reetz, Thomas Kropf:
Simplifying Deep Embedding: A Formalised Code Generator.
378-390
- Klaus Schneider, Ramayya Kumar, Thomas Kropf:
Automating Verification by Functional Abstraction at the System Level.
391-406
- Konrad Slind:
A Parameterized Proof Manager.
407-423
- Sofiène Tahar, Ramayya Kumar:
Implementational Issues for Verifying RISC-Pipeline Conflicts in HOL.
424-439
- Phillip J. Windley:
Specifying Instruction-Set Architectures in HOL: A Primer.
440-455
- Joakim von Wright:
Representing Higher-Order Logic Proofs in HOL.
456-470
Last update Fri May 25 08:43:21 2012
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
