Mechanizing Execution Sequence Semantics in HOL

Gavan Tredoux Laboratory for Formal Aspects and Complexity in Computer Science, Department of Mathematics, University of Cape Town.

Abstract

The mechanization in Higher Order Logic of a general-purpose operational semantics for programming languages is described. The mechanization allows the sound derivation of Dijkstra-style axiomatic semantics. A small programming language fragment is presented as an illustration Keywords: HOL, Mechanized Proof, Program semantics, Weakest preconditions Computing Review Categories: D.2.4, D.3.1, F.3.1, F.3.2, F.4.1

1 Introduction

This paper describes a mechanization, in the interactive theorem-prover HOL, of a general-purpose semantics for programming languages, based on execution sequences. This provides an environment in which a wide class of formalisms for reasoning about programs can be mechanized, including Dijkstra’s algebra of weakest preconditions, dynamic logic and Hoarestyle specifications. The aim is to show that execution sequences provide a mathematically ‘clean’ semantics for programming languages that is straightforward to mechanize in HOL, and properly models both bounded and unbounded non-determinism. This is in contrast to other semantics for non-determinism, for instance powerdomain constructions, whose mathematical sophistication makes mechanization in HOL more difficult.

2 An Overview of HOL

HOL is a proof assistant and verifier, descended from the LCF family of theorem provers [11, 17], embedding a higher-order logic in a functional programming language, ML [9]. The system guarantees adherence to the logic by isolating its axioms and primitive rules of inference in an abstract data type, thm. The strongly typed nature of ML ensures that theorems (objects of type thm) can only be obtained from the axioms and primitive rules of inference. The embedding in ML also allows an arbitrary degree of mechanization, in the form of derived rules of inference and proof strategies, while still guaranteeing soundness. This is in contrast to non-inferential approaches to theorem proving, which often deliver ‘theorems’ after complicated rewriting and resolution procedures without guaranteeing the soundness of those procedures. To date, HOL has been used mostly for the specification and verification of hardware [6], but the expressive power of higher-order logic captures, in principle, anything that is mathematically tractable [5, 10].

The HOL logic is based on Church’s Simple Theory of Types [7, 1], and is essentially Predicate Calculus enriched with typed lambda calculus. Variables may range over functions, and the arguments of functions may themselves be functions. Each term of the logic must be well-typed, having a type consistent with the types of its subterms. HOL has a number of built in types, for example boolean values bool, natural numbers num, and strings string. There are also type constructors, which construct new types from existing ones (for example function spaces between types, lists of elements of a type) and facilities for adding new types to the logic. Denote a typed term by t:σ where t is a term and σ is its type. For example, denote a variable x of type bool by x:bool. Most of the constructs of the predicate calculus are implemented straightforwardly in HOL, but some unusual features of the logic worth noting are:

• Predicates are functions with range bool. For example λn:num.n<5 is a predicate on the natural numbers, mapping any natural number to T (for true) or F (for false), depending on whether it is less than 5 or not. A set of values of some type may be represented by its membership predicate on that type.

• Hilbert’s ε-operator plays an important role. If P is a predicate over values of type σ, then εx:σ.Px is an unspecified but fixed variable x of type σ , such that if anything satisfies the predicate P, then x satisfies P - if nothing satisfies P then εx:σ.Px is an unspecified but fixed value of type σ. More formally, it is an axiom of the logic that if ⊢∃x.Px , then ⊢P(εx.Px) [12, 1].

• There is notation for conditional statements. ‘If c then d else e’ is denoted by ‘c⇒d|e’.

• The type discipline is polymorphic, so that terms with variable types are allowed [14]. Proof in HOL is by natural deduction; theorems are obtained by rules of inference from axioms and previously proved theorems, in the ‘forward’ direction. HOL also supports simulation of ‘backward’ goal-directed proof, through the use of Milner’s tactics [15], which automatically translate goal-directed ‘proofs’ into forward proofs [16].

The HOL logic can be extended by postulating new axioms, which risks the introduction of inconsitency, or by definition, which is conservative in that it cannot introduce inconsistency [13]. There are three mechanisms for making new definitions:

• Type definition. A new type can be introduced as a non-empty named subset of an existing type, by providing an isomorphism from the new type to the subset, and proving that the subset is nonempty. New type operators may also be defined, and there are facilities for defining a restricted class of recursive types [13].

• Constant definition. A new constant can be introduced as a non-recursive abbreviation for a term in the logic.

• Constant specification. If it can be proved that ⊢∃x.Px , then a constant c can be introduced satisfying ⊢Pc . This allows partial specification, where P fixes only certain properties of the constant and not others; for example, a total function could be introduced by specifying its behaviour on a subset of its domain and leaving it unspecified elsewhere. The extensive use of definitions entails that proofs

rely heavily on rewriting routines; these are implemented as derived rules of inference in ML procedures, guaranteeing soundness. ML is itself a higher-order functional language (functions may take functions as arguments) so that rewriting routines may be soundly tailored by the user to specific situations, in arbitrarily complex ways. The soundness of user extensions to inference mechanisms poses a difficult problem for most theorem-provers not in the LCF fold [3].

Extensions of the logic are organized hierarchically in theories; named collections of types, type operators, constants, definitions, axioms and theorems. A library of commonly used theories is built-in, for example theories concerning sets, the natural numbers and finite-length lists. The expressive power of the HOL logic, due to its higher-order variables and type polymorphism, allows the formulation and proof of very general definitions and lemmas, which can be reused in many different contexts. The extent to which this simplifies mechanization will be revealed later in this paper.

3 Execution Sequence Semantics

Only an overview of execution sequence semantics can be given here; for a more detailed treatment see [4], where a similar semantics is used to model Dijkstra’s algebra of weakest preconditions [8]. Execution sequences (exseqs) are sequences of machine states, where the states are left undefined, of one of the following kinds:

• Finite and properly terminated.

Denoted by < s_{1}, s_{2}, s_{3}, …, s_{n} >, where the s_{i} are states.

• Finite and improperly terminated. Denoted by < s_{1}, s_{2}, s_{3}, …, s_{n}).

• Infinite, non-terminating.

Denoted by < s_{1}, s_{2}, s_{3}, …, s_{n}, …).

Each exseq thus represents a computation path, starting at the first state in the sequence and proceeding through the remaining states. Aborted computation is distinguished from non-termination as improper termination. Denote an arbitrary exseq by < s_{1}, s_{2}, s_{3}, …, s_{n}, … >, which may be of any of the above kinds. The following operations on exseqs are essential for defining the semantics of programs (note that the operations are only defined for the kinds of exseqs indicated):

• first< s_{1}, s_{2}, s_{3}, …, s_{n}, … > = s_{1}.

• last< s_{1}, s_{2}, s_{3}, …, s_{n} > = s_{n}.

• length< s_{1}, s_{2}, s_{3}, …, s_{n} > = n, length< s_{1}, s_{2}, s_{3}, …, s_{n}) = n, length< s_{1}, s_{2}, s_{3}, …, s_{n}, …) = ω.

• < s_{1}, s_{2}, s_{3}, …, s_{n} >join< t_{1}, t_{2}, …, t_{n}, … > = < s_{1}, s_{2}, …, s_{n}, t_{2}, …, t_{n}, … > where s_{n} = t_{1}. Note that the resulting exseq has the same subtype as the second exseq, that the intermediate state is not repeated, and that the join is undefined where s_{n} ≠ t_{1}. Programs are identified with sets of exseqs, with each exseq a possible computation path. This models non-determinism by allowing a program to contain exseqs starting from the same state; the program may follow any of its possible computation paths starting from such a state, non-deterministically. Programs may be said to be deterministic if they have no more than one exseq starting in any state. As programs are sets, they may be combined using the usual settheoretic operations, for example union and intersection, and are completely specified by their elements. Let S be the set of all machine states, and then define the following fragment of a programming language:

• skip= {< s, s >| sϵS}, a program which does nothing and then terminates.

• P ;; Q = {e join d | eϵP and dϵQ and the join is defined} ∪ {e | eϵP and e does not terminate properly}, sequential composition of two programs.

• P || Q = P ∪ Q, non-deterministic choice between programs, modelled by set-theoretic union. In the model chosen here, every program computation does something so that skip is treated as an identity mapping between states, rather than a program which does nothing, for instance one which contains only singleton exseqs. This is a next-state relation: intermediate states are significant. Models in which intermediate states are not significant use an input-output relation, for example Dijkstra’s algebra of weakest preconditions. Hence skip is not an identity with respect to sequential composition, as the first example below shows:

• skip ;; skip= {< s, s, s >| sϵS}

• (skip) || (skip ;; skip) = {< s, s >| sϵS} ∪ {< s, s, s >| sϵS}. This is because skip is treated as a program which

does not alter a state, but nevertheless performs a computation. Of course, viewed in terms of the inputoutput relation, skip alters neither input nor output, and hence ‘does nothing.’

Note that the use of union to model nondeterministic choice diverges from [4], who use Hilbert’s ε-operator, with some unfortunate consequences. Defining for programs P and Q P || Q = ε x· (x=P)∨(x=Q), entails that:

• If P and Q are deterministic then P || Q is deterministic, so that no new non-determinism is introduced. Which program ε chooses is fixed and unspecified, but it is either P or Q, and so it must be deterministic.

• (P || Q) ;; (P || Q) is either the program P ;; P or the program Q ;; Q, since what ε chooses is fixed. This excludes the possibilities P ;; Q and Q ;; P, which is most undesirable. The use of union to model non-deterministic

choice can include sequences and some of their (initial) subsequences in the same program, as the example (skip) || (skip ;; skip) above demonstrates; contrast this with [4], where ε was used specifically to exclude subsequences. This extends non-determinism to include termination, for it is not determined whether in a state that is the last of a subsequence, the program will terminate, ie. it is on the computation path represented by the subsequence, or proceed to compute, ie. it is on the computation path represented by the supersequence. This notion of non-determinism was raised but not pursued in [4].

4 Representing Execution Sequences

Execution sequences are represented in the HOL logic, forming an extension of that logic; they are defined in terms of constructs of the logic already present, using the type definition and constant definition facilities outlined above. It is worth emphasizing that this is a conservative extension of the logic - soundness is guaranteed - and that an axiomatic definition of execution sequences, while it would appear to be more natural and would entail less work, would carry the danger of introducing inconsistency.

To represent execution sequences, a more concrete notion of ‘machine state’ is needed; here states are simply thought of mappings from variables (identified by character strings) to their values (which are just natural numbers). This may be defined in HOL as the following type abbreviation:

 new_type_abbrev(`state`,":string->num");;

The type of execution sequences is defined in HOL as a disjoint union of sub-types of finite and infinite sequences, where an infinite sequence of states is represented by a mapping from numbers to states f:num→state indexing the elements, and a finite sequence by a tuple (f, n), where f:num→state indexes the elements, and n represents the length. To ensure that the finite sequences are non-empty, and that each exseq is uniquely represented by a tuple (f, n), we require that 0 < n, and that f(i) be an arbitrary but fixed constant where n ≤ i, so that values of f which do not represent elements represent nothing. Thus the type of finite sequences is defined as that subset of the cartesian product (f:num→state)⊗(num) satisfying the above conditions on f and n.^{1}

The facilities in HOL for defining new types allow ‘free type definitions’ using a BNF-style syntax, so that existing types may be easily combined in disjoint unions. These are used to combine finite and infinite sequences to form exseqs, as the following HOL type definition shows:

 let exseq = define_type `exseq`
     `exseq = FIN (state)finseq
               | INF (num->state)
               | INC (state)finseq`;;

Thus, an exseq is either a finite sequence of states labelled FIN, an infinite sequence labelled INF, or a finite sequence labelled INC. These labellings correspond to properly terminated exseqs, non-terminating exseqs, and improperly terminated exseqs, respectively. To facilitate reasoning about the lengths of sequences, the type of natural numbers num is extended to include ω, forming the new type, w nat, and a partial order on w nat, denoted by ‘<!’, is defined in the obvious way:

 let w_nat =
     define_type `w_nat` `w_nat = OMEGA | NAT num`;;

Since exseqs have been divided into different subtypes, there must be a way of explicitly determining the subtype of any exseq; these tests will play an important role in the examples that follow. We will also need a way of getting the ‘n’ out of ‘NAT n’, if we want to add and subtract lengths of finite sequences. The following functions perform these operations, and are defined in HOL by cases, using the structure of the types exseq and w nat. Here TERM, INFI and INCP are boolean functions which return T if their arguments are finite and properly terminated, finite but not properly terminated, or infinite (nonterminating), respectively. The function val will strip the NAT label off an element of w nat to return a natural number, and is undefined for OMEGA.

1This is a simplification: a type of finite sequences of elements

of any type σ, (σ)finseq, is defined, and a finite sequence of

states is instantiated as (state)finseq – but this is not to our

purpose here.

let TERM =
new_recursive_definition false exseq `TERM`
"(TERM (FIN s :exseq) = T) /\
(TERM (INF f :exseq) = F) /\
(TERM (INC s :exseq) = F)";;
let INFI =
new_recursive_definition false exseq `INFI`
"(INFI (FIN s : exseq) = F) /\
(INFI (INF f : exseq) = T) /\
(INFI (INC s : exseq) = F)";;
let INCP =
new_recursive_definition false exseq `INCP`
"(INCP (FIN s : exseq) = F) /\
(INCP (INF f : exseq) = F) /\
(INCP (INC s : exseq) = T)";;
let val =
new_recursive_definition false w_nat `val`
"val (NAT n) = n";;

Exseqs satisfy some fundamental properties which provide an abstract characterization, or specification, of them, and which must be derived from any representation to establish that they have been correctly represented. For instance, any exseq is completely determined by its elements, length and subtype (FIN, INF or INC); this is captured by the following HOL theorem, derived directly from the definitions involved: ⊢ ∀x y. x sametype exseq y ⟹

(length x = length y) ∧ (∀ n. (NAT n) <! (length x)

⟹ (element n x = element n y)) ⟹(x = y) Thus, exseqs of the same subtype with the same

length and the same elements are equal, and therefore the representation of exseqs is well-defined. A mechanism for explicitly constructing exseqs containing particular states must also be defined; for the purposes of program semantics, only singletons and pairs need to be explicitly constructed. The following theorems establish the correctness of the constructions, where sng(s) returns a singleton exseq containing just the state s, and pair(s, t) returns an exseq containing just the states s and t: ⊢ ∀s:state. length(sng s) = NAT 1 ⊢ ∀s:state. first(sng s) = s ⊢ ∀s:state. last(sng s) = s ⊢ ∀s t:state. length(pair(s, t)) = NAT 2 ⊢ ∀s t:state. first(pair(s, t)) = s ⊢ ∀s t:state. last(pair(s, t)) = t

The following theorems establish the correctness of the representation of the join function, by describing the length of the join and the elements it contains. ⊢ ∀e d:exseq. (first d = last e) ⟹TERM e ⟹

∀n:num. ((NAT n <! (length e)) ⇒ (element n (e join d) = element n e) | ((NAT n <! length(e join d)) ⟹ (element n (e join d) =

element(1+n-(val(length e))) d)))

⊢ ∀e d:exseq. (first d = last e) ⟹TERM e ⟹ (INFI d ⇒ (length(e join d) = OMEGA) | (val(length(e join d)) =

val(length e) + val(length d) - 1))

Thus e join d, if it is defined (ie. e terminates cleanly and the last of e is the first of d) has all the elements of e and all the elements of d except its first, in that order. ^{2}

length(e join d) = OMEGA

if d is infinite, non-terminating val(length(e join d)) =

val(length e) + val(length d)-1 if d is finite

Since exseqs are completely characterized by their elements and length, the above theorems alone establish the correctness of the representations of the functions involved.

5 Representing Programs

As a program is a set of execution sequences, and sets may be identified with their membership predicates, each program can be represented as a predicate on the type of execution sequences. This allows partial programs, which might not have any execution sequences starting from some states. As programs are predicates, they may be combined using the usual logical operators, and are easy to manipulate in HOL. Moreover, specification languages like Dijkstra’s calculus of weakest preconditions and Hoare-style assertions, can now be expressed very naturally in the logic. As specifications employ the notion of predicates on states, the following type abbreviations are useful:

 new_type_abbrev(`command`, ":exseq -> bool");;
 new_type_abbrev(`pred`, ":state -> bool");;

Thus commands are mappings from exseq to bool, while predicates on states are mappings from state to bool. Since we are allowing partial commands, to model partial programs, determining the domain of a command will be useful. Moreover, a test for determinism, or lack of it, is essential. The following function constants are defined accordingly:

dom = ⊢_{Def} ∀c:command. ∀s:state.

dom c = λs:state. ∀e:exseq. c e ∧ (first e = s)

det = ⊢_{Def} ∀c:command.

det c = ∀e_{1} e_{2}:exseq.

(c e_{1})⟹(c e_{2})⟹
(first e_{2} = first e_{1})⟹
(e_{1} = e_{2})

The HOL definitions for the programming language fragment discussed above now follow naturally from their set-theoretic counterparts, where ‘;;’ sequences commands, and ‘ || ’ chooses between two commands, non-deterministically: skip = ⊢_{Def} skip = λp:exseq. ∃s:state.

2We had to use val to manipulate the lengths as natural num-

bers, to perform addition and subtraction. Note that the

intermediate state is not repeated in the join

p = pair(s, s)

seq = ⊢_{Def} ∀c_{1} c_{2}:command. c_{1} ;; c_{2} = λe:exseq. ((c_{1} e) ∧(¬TERM e)) ∨ (∃e_{1} e_{2}:exseq.(c_{1} e_{1}) ∧ (TERM e_{1}) ∧

(c_{2} e_{2}) ∧ (first e_{2} = last e_{1}) ∧ (e = e_{1} join e_{2}))

choose = ⊢_{Def} ∀c_{1} c_{2}:command.

c_{1} || c_{2} = λe:exseq. (c_{1} e)∨(c_{2} e)

Programming constructs have thus been directly represented in the HOL logic; programs can be translated into terms of the logic, where each program is of the type command. This facilitates proving properties of particular programs, for example correctness with respect to weakest precondition specifications, but has the drawback that there is no way of formulating theorems about a particular language as a whole. Theorems may quantify over particular commands only, or over commands as a whole. For example, there is no way of asserting that every program in the fragment introduced above is total, although this is certainly true. This can be remedied by defining a recursive type that represents the language as a syntactic entity, and then recursively associating constructs of the language with terms in the logic of type command, via a ‘Meaning’ function in classical denotational style. The HOL code below does this for the programming fragment:

let fragment = define_type `fragment`
`fragment = SKIP
| SEQ fragment fragment
| CHOOSE fragment fragment`;;
let Meaning = new_recursive_definition
false fragment `Meaning`
"(Meaning SKIP = Skip) /\
(Meaning (SEQ f1 f2) =
(Meaning f1) ;; (Meaning f2)) /\
(Meaning (CHOOSE f1 f2) =
(Meaning f1) || (Meaning f2))";;

Dijkstra’s weakest precondition operator [8] has become central to many program specification and transformation schemes, and embedding this in a theorem proving environment allows proof of the soundness of specifications and the correctness of transformations [2]. The definition in HOL is straightforward: wp = ⊢_{Def} ∀c:command. ∀R:pred. ∀s:state.

wp c R = λs:state. ∀e:exseq. (c e) ⟹ (first e = s) ⟹ ((TERM e) ∧ (R (last e)))

Thus for any command c, wp c is a mapping from pred to pred, ie. a predicate transformer. For any predicate on states R, wp c R is a predicate that is satisfied by those states from which, if c is defined at those states, c is bound to terminate in a state satisfying R. The following definitions facilitate manipulation of predicates on states: false = ⊢_{Def} false = λs:state. F true = ⊢_{Def} true = λs:state. T OR = ⊢_{Def} ∀P Q:pred.

P OR Q = λs:state. P s ∨ Q s

AND = ⊢_{Def} ∀P Q:pred.

P AND Q = λs:state. P s ∧ Q s

IMPLIES = ⊢_{Def} ∀P Q:pred.

P IMPLIES Q = λs:state.

(P s) ⟹ (Q s)

Dijkstra formulates a number of ‘Healthiness Conditions’, identities involving the weakest precondition operator which any program ought to satisfy, provided that the weakest precondition operator and the programming semantics have been correctly defined. These can be derived formally in HOL from the definitions given above. ⊢ ∀c:command.

(dom c = true) ⟹ (wp c false = false) ⊢ ∀c:command. ∀Q R:pred.

(wp c Q) AND (wp c R) = wp c (Q AND R) ⊢ ∀c:command. ∀Q R:pred.

(((wp c Q) OR (wp c R)) IMPLIES (wp c (Q OR R)))

= true

⊢ ∀c:command. ∀Q R:pred. det c ⟹ ((wp c Q) OR (wp c R) = wp c (Q OR R)) The above results, unless indicated otherwise,

hold for any command. In particular they hold for non-deterministic commands, and it is a major strength of the execution sequence approach that this is cleanly handled for both the bounded and unbounded cases. The non-determinism exhibited by a program is said to be bounded if for every state the program contains at most a finite number of possible computation paths starting at that state, and unbounded if for some state there is an infinite number of possible computation paths. As commands are arbitrary sets of exseqs (computation paths), any kind of nondeterminism may be present. Other mechanizations of programming formalisms in HOL have either failed to model Dijkstra’s Healthiness conditions in the presence of non-determinism in general [10], or have not fully catered for unbounded non-determinism [2].

Dijkstra-style specifications of the semantics of the programming fragment introduced above can be derived, verifying the reasonableness of the definitions given using the execution-sequence semantics. ⊢ ∀R:pred. wp skip R = R ⊢ ∀c_{1} c_{2}. ∀R:pred.

wp (c_{1} ;; c_{2}) R = wp c_{1} (wp c_{2} R) ⊢ ∀c_{1} c_{2}:command. ∀R:pred.

wp (c_{1} || c_{2}) R = (wp c_{1} R) AND (wp c_{2} R)

To give the reader some idea of the mechanics of HOL proof, the ML code that constructs the proof of the last theorem is exhibited (notice that HOL uses ‘!’ for ∀). Not all of the proofs of the above properties were this short, the proof of sequential composition running to over a page of code.

let choose_wp = prove_thm (
`choose_wp`,
"!c1 c2 R. wp (c1 || c2) R =
                 (wp c1 R) AND (wp c2 R)",
CONV_TAC (DEPTH_CONV FUN_EQ_CONV)
THEN REWRITE_TAC [wp;choose;AND]
THEN CONV_TAC (DEPTH_CONV BETA_CONV)
THEN REWRITE_TAC [ANTE_DISJ_IMP]
THEN CONV_TAC (DEPTH_CONV FORALL_AND_CONV)
THEN REWRITE_TAC[]
);;

The purpose of this paper has been to show that HOL provides a natural vehicle for mechanizing execution sequence semantics, with a view to mechanizing formalisms for specifying and proving properties of programs; thus the programming fragment above was intended to illustrate the principles involved. This is the subject of ongoing research by the author.

References

1. P Andrews. An Introduction to Mathematical Logic and Type Theory: to Truth through Proof. Computer Science and Applied Mathematics Series. Academic Press, 1986.

2. R Back and J von Wright. ‘Refinement concepts formalised in Higher Order Logic’. Formal Aspects of Computing, 2(3):247–272, (July-September 1990).

3. R Boyer and J Moore. ‘Metafunctions: Proving them correct and using them efficiently as new proof procedures’. In R Boyer and J Moore, eds., The Correctness Problem in Computer Science. Academic Press, New York, (1981).

4. C Brink and I Rewitzky. ‘Modelling the algebra of weakest preconditions’. In Proceedings of the 6th Southern African Computer Symposium, Caledon, 2-3 July 1990, pp. 242–261. Also to appear in the South African Computer Journal.

5. A Camilleri. ‘Mechanizing CSP trace theory in Higher Order Logic’. IEEE Transactions on Software Engineering, 16(9):993–1004, (September 1990).

6. A Camilleri, M Gordon, and T Melham. ‘Hardware verification using higher-order logic’. In D Borrione, ed., From HDL Descriptions to Guaranteed Correct Circuit Designs, pp. 43–67. Proceedings of the IFIP WG 10.2 Working Conference, Grenoble, September 1986, North-Holland, (1987).

7. A Church. ‘A formulation of the simple theory of types’. Journal of Symbolic Logic, 5:56–68, (1940).

8. E Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

9. M Gordon. ‘HOL: A proof generating system for higher-order logic’. In G Birtwistle and P Subrahmanyan, eds., VLSI Specification, Verification and Synthesis, Kluwer International Series in Engineering and Computer Science, pp. 73–128. Kluwer Academic Publishers, Boston, (1988).

10. M Gordon. ‘Mechanizing programming logics in higher order logic’. In G Birtwistle and P Subrahmanyam, eds., Current Trends in Hardware Verification and Automated Theorem-Proving, pp. 387– 439. Springer-Verlag, (1989).

11. M Gordon, R Milner, and C Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

12. A Leisenring. Mathematical Logic and Hilbert’s ϵ-Symbol. University Mathematical Series. Macdonald & Co. Ltd., London, 1969.

13. T Melham. ‘Automating recursive type definitions in Higher Order Logic’. In G Birtwistle and P Subrahmanyam, eds., Current Trends in Hardware Verification and Automated Theorem Proving, pp. 341–386. Springer-Verlag, (1989).

14. R Milner. ‘A theory of type polymorphism in programming’. Journal of Computer and System Sciences, 17:348–375, (1978).

15. R Milner. ‘The use of machines to assist in rigorous proof’. Philosophical Transactions of the Royal Society of London A, 312:411–422, (1984).

16. L Paulson. ‘A higher-order implementation of rewriting’. Science of Computer Programming, 3:119–149, (1983).

17. L Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge Tracts in Theoretical Computer Science 2. Cambridge University Press, 1987.