Higher Order Logic Theorem Proving and Its Applications Book

	LCF Examples in HOL	1
	A Graphical Tool for Proving UNITY Progress	17
	Reasoning About a Class of Linear Systems of Equations in HOL	33
	Towards a HOL Theory of Memory	49
	Providing Tractable Security Analyses in HOL	65
	Highlighting the Lambda-free Fragment of Automath	81
	First-Order Automation for Higher-Order-Logic Theorem Proving	97
	Symbolic Animation as a Proof Tool	113
	Datatypes in L2	128
	A Formal Theory of Undirected Graphs in Higher-Order Logic	144
	Mechanical Verification of Distributed Algorithms in Higher-Order Logic	158
	Tracking Design Changes with Formal Verification	177
	Weak Systems of Set Theory Related to HOL	193
	Interval-Semantic Component Models and the Efficient Verification of Transaction-Level Circuit Behavior	205
	An Interpretation of NODEN in HOL	221
	Reasoning about Real Circuits	235
	Binary Decision Diagrams as a HOL Derived Rule	254
	Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition Generator	269
	S : A Machine Readable Specification Notation Based on Higher Order Logic	285
	An Engineering Approach to Formal Digital System Design	300
	Generating Designs Using an Algorithmic Register Transfer Language with Formal Semantics	316
	A HOL Formalisation of the Temporal Logic of Actions	332
	Studying the ML Module System in HOL	346
	Towards a Mechanically Supported and Compositional Calculus to Design Distributed Algorithms	362
	Simplifying Deep Embedding: A Formalised Code Generator	378
	Automating Verification by Functional Abstraction at the System Level	391
	A Parameterized Proof Manager	407
	Implementational Issues for Verifying RISC-Pipeline Conflicts in HOL	424
	Specifying Instruction-Set Architectures in HOL: A Primer	440
	Representing Higher Order Logic Proofs in HOL	456