Higher Order Logic Theorem Proving and Its Applications

Part 1 Mathematical logic: the HOL logic extended with quantification over type variables, T.F. Melham; a lazy approach to fully-expansive theorem proving, R.J. Boulton; efficient representation and computation of tableaux proofs, K. Schneider et al; a note on interactive theorem proving with theorem continuation functions, C.-T. Chou; a sequent formulation of a logic of predicates in HOL, C.-T. Chou; a classical type theory with transfinite types, G. Pottinger. Part 2 Induction: unification-based induction, H. Busch; introducing well-founded function definitions in HOL, M. van der Voort; Boyer-Moore automation for the HOL system, R.J. Boulton. Part 3 General modelling and proofs: constructing the real numbers in HOL, J. Harrison; modelling generic hardware structures by abstract datatypes, K. Schneider et al; a methodology for reusable hardware proofs, M. Aagaard and M. Leeser; abstract theories in HOL, P.J. Windley; machine abstraction in microprocessor specification, M. McAllister. Part 4 Formalizing and modelling of automata: a formal theory of simulations between infinite automata, P. Loewenstein; a comparison between statecharts and state transition assertions, N. Day; an embedding of timed transition systems in HOL, R. Cardell-Oliver et al; formalizing a modal logic for CSS in the HOL theorem prover, M. Nesi; modelling non-deterministic systems in HOL, J. Alves-Foss. Part 5 Program verification: mechanizing some advanced refinement concepts, J. von Wright et al; deriving correctness properties of compiled code, P. Curzon; a HOL mechanization of the axiomatic semantics of a simple distributed programming language, W.L. Harrison et al. Part 6 Hardware description language semantics: a formalization of the VHDL simulation cycle, J.P. van Tassel; the formal semantics definition of a multi-rate DSP specification language in HOL, C. Angelo et al; design-flow graph partitioning, R.B. Hughes and G. Musgrave. Part 7 Hardware verification methodologies: implementation and use of annotations in HOL, S. Kalvala et al; towards a formal verification of a floating point coprocessor and its composition with a central processing unit, J. Pan et al; deriving a correct computer, L.-G. Wang; formal tools for tri-state design in busses, R.B. Hughes et al; specification and formal synthesis of digital circuits, M. Bombana et al. Part 8 Simulation in higher order logic: operational semantics based formal symbolic simulation, K.G.W. Goosens; simulating microprocessors from formal specifications, K.M. Hall and P.J. Windley; executing HOL specifications - towards an evaluation semantics for classical higher order logic, P.S. Rajan. Part 9 Extended uses of higher order logic: linking other theorem provers to HOL using PM - proof manager, M. Archer et al; adding new rules to an LCF-style logic implementation, K. Slind; why we can't have SML style declarations in HOL, E.L. Gunter.