Higher order logic theorem proving and its applications : proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and Its Applications--HOL '92
Ifip Tc, Luc Claesen, Michael J. C. Gordon · North-Holland eBooks · 1993
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.