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. Springer 1994 Lecture Notes in Computer Science 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
- 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
- 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
- I. S. W. B. Prasetya: Towards a Mechanically Supported and Compositional Calculus to Design Destributed Algorithms. 362-377
- 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
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-19T203413 by the dblp team