Abstract is missing.
- Program Verification using HOL-UNITYFlemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson. 1-15
- Graph model of LAMBDA in Higher Order LogicKim Dam Petersen. 16-28
- Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOLCui Zhang, Robert J. Shaw, Ronald A. Olsson, Karl N. Levitt, Myla Archer, Mark Heckman, Gregory D. Benson. 29-42
- Reasoning with the Formal Definition of Standard ML in HOLDon Syme. 43-60
- HOL-MLMyra Van Inwegen, Elsa L. Gunter. 61-74
- Stucture and Behaviour in Hardware VerificationKees G. W. Goossens. 75-88
- Degrees of Formality in Shallow Embedding Hardware Description Languages in HOLCatia M. Angelo, Luc J. M. Claesen, Hugo De Man. 89-100
- A Functional Approach for Formalizing Regular Hardware StructuresDirk Eisenbiegler, Klaus Schneider, Ramayya Kumar. 101-114
- A Proof Development System for HOLLaurent Théry. 115-128
- A HOL Package for Reasoning about Relations Defined by Mutual InductionRachel E. O. Roxas. 129-140
- A Broader Class of Trees for Recursive Type Definitions for HOLElsa L. Gunter. 141-154
- Some Theorems We Should ProveDavid Lorge Parnas. 155-162
- Using PVS to Prove Some Theorems Of David ParnasJohn M. Rushby, Mandayam K. Srivas. 163-173
- Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the RealsJohn Harrison, Laurent Théry. 174-184
- The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-ProverJeffrey J. Joyce, Carl-Johan H. Seger. 185-198
- Linking HOL to a VLSI CAD SystemJuin-Yeu Lu, Shiu-Kai Chin. 199-212
- Alternative Proof Procedures for Finite-State Machines in Higher-Order LogicKlaus Schneider, Ramayya Kumar, Thomas Kropf. 213-226
- A Formalization of Abstraction in LAMBDAAnthony McIsaac. 227-238
- Report on the UCD Microcoded Viper Verification ProjectTej Arora, Tony Leung, Karl N. Levitt, E. Thomas Schubert, Phillip J. Windley. 239-252
- Verification of the Tamarack-3 Microprocessor in a Hybrid Verification EnvironmentZheng Zhu, Jeffrey J. Joyce, Carl-Johan H. Seger. 253-266
- Abstraction Techniques for Modeling Real-World Interface ChipsDavid A. Fura, Phillip J. Windley, Arun K. Somani. 267-280
- Implementing a Methodology for Formally Verifying RISC Processors in HOLSofiène Tahar, Ramayya Kumar. 281-294
- Domain Theory in HOLSten Agerholm. 295-309
- Predicates, Temporal Logic, and SimulationsChing-Tsun Chou. 310-323
- Formalization of Variables Access Constraints to Support Compositionality of Liveness PropertiesI. S. W. B. Prasetya. 324-337
- The Semantics of Statecharts in HOLNancy A. Day, Jeffrey J. Joyce. 338-351
- Value-Passing CCS in HOLMonica Nesi. 352-365
- TPS: An Interactive and Automatic Tool for Proving Theorems of Type TheoryPeter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi. 366-370
- Modelling Bit Vectors in HOL: the word libraryWai Wong. 371-384
- Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware VerificationKlaus Schneider, Ramayya Kumar, Thomas Kropf. 385-398
- Toward a Super Duper Hardware TacticMark Aagaard, Miriam Leeser, Phillip J. Windley. 399-412
- A Mechanisation of Name-Carrying Syntax up to Alpha-ConversionAndrew D. Gordon. 413-425
- A HOL Decision Procedure for Elementary Real AlgebraJohn Harrison. 426-435
- AC Unification in HOL90Konrad Slind. 436-449
- Server-Process Restrictiveness in HOLStephen H. Brackin, Shiu-Kai Chin. 450-463
- Safety in Railway Signalling Data: A Behavioural AnalysisMatthew J. Morley. 464-474
- On the Style of Mechanical ProvingI. S. W. B. Prasetya. 475-488
- From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic SimulationSreeranga P. Rajan, Jeffrey J. Joyce, Carl-Johan H. Seger. 489-500
- Verification in Higher Order Logic of Mutual Exclusion AlgorithmVictor Carreño. 501-513
- Using Isabelle to Prove Simple TheoremsSara Kalvala. 514-517