Abstract is missing.
- LCF Examples in HOLSten Agerholm. 1-16
- A Graphical Tool for Proving Unity ProgressFlemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson. 17-32
- Reasoning About a Class of Linear Systems of Equations in HOLCatia M. Angelo, Luc J. M. Claesen, Hugo De Man. 33-48
- Towards a HOL Theory and MemoryJean-Paul Bodeveix, Mamoun Filali, P. Roche. 49-64
- Providing Tractable Security Analysis in HOLStephen H. Brackin. 65-80
- Highlighting the Lambda-free Fragment of AutomathN. G. de Bruijn. 81-96
- First-Order Automation for Higher-Order-Logic Theorem ProvingHolger Busch. 97-112
- Symbolic Animation as a Proof ToolJuanito Camilleri, Vincent Zammit. 113-127
- Datatypes in L2Nick Chapman, Simon Finn, Michael P. Fourman. 128-143
- A Formal Theory of Undirected Graphs in Higher-Order LogicChing-Tsun Chou. 144-157
- Mechanical Verification of Distributed Algorithms in Higher-Order LogicChing-Tsun Chou. 158-176
- Tracking Design Changes with Formal VerificationPaul Curzon. 177-192
- Weak Systems of Set Theory Related to HOLThomas Forster. 193-204
- Interval-Semantic Component Models and the Efficient Verification of Transaction-Level Circiut BehaviorDavid A. Fura, Arun K. Somani. 205-220
- An Interpretation of NODEN in HOLBrian T. Graham. 221-234
- Reasoning about Real CircuitsKeith Hanna. 235-253
- Binary Decision Diagrams as a HOL Derived RuleJohn Harrison. 254-268
- Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition GeneratorPeter V. Homeier, David F. Martin. 269-284
- S: A Machine Readable Specification Notation based on Higher Order LogicJeffrey J. Joyce, Nancy A. Day, Michael R. Donat. 285-299
- An Engineering Approach to Formal Digital System DesignMats Larsson. 300-315
- Generating Designs Using an Algorithmic Register Transfer Language with Formal SemanticsJuin-Yeu Lu, Shiu-Kai Chin. 316-331
- A HOL Formalisation of the Temporal Logic of ActionsThomas Långbacka. 332-345
- Studying the ML Module System in HolSavi Maharaj, Elsa L. Gunter. 346-361
- Towards a Mechanically Supported and Compositional Calculus to Design Destributed AlgorithmsI. S. W. B. Prasetya. 362-377
- Simplifying Deep Embedding: A Formalised Code GeneratorRalf Reetz, Thomas Kropf. 378-390
- Automating Verification by Functional Abstraction at the System LevelKlaus Schneider, Ramayya Kumar, Thomas Kropf. 391-406
- A Parameterized Proof ManagerKonrad Slind. 407-423
- Implementational Issues for Verifying RISC-Pipeline Conflicts in HOLSofiène Tahar, Ramayya Kumar. 424-439
- Specifying Instruction-Set Architectures in HOL: A PrimerPhillip J. Windley. 440-455
- Representing Higher-Order Logic Proofs in HOLJoakim von Wright. 456-470