default search action
7th TPHOLs 1994: Valletta, Malta
- Thomas F. Melham, Juanito Camilleri:
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
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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-29 01:14 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: