Computer Aided Formal Reasoning 1996/7 Lecture notes 16 Judith Underwood

Reasoning about imperative programs

All of the material here is taken from Gries, The Science of Programming, Springer-Verlag, 1981. This is a good book to buy if you’re interested in this approach.

Up til now, we have been reasoning about purely functional programs. Functional programs are easier to prove things about, because the entire behaviour of a function f can be described by the relationship between x and (f x). There are no “side-effects” like assignment which change the environment.

On the other hand, imperative programs are much more common. Imperative programs may change parts of an external state (e.g. values stored in variables) as it executes. Thus, the state must be included in any description of the behaviour of a program. This means we will need a way of referring to the state before a program executes, and the state afterwards.

We describe a state by giving a logical description of the variables we are interested in. For example, we may describe a state by the formula

x = 5 ∧ x < y.

This really describes a collection of states, partly because there may be many values of y, but also because there may be variables s, t, w, and z as well, and we have not specified anything about them.

Given such descriptions of states, we describe the execution of a program by means of triples like

{Q}S{R}

means “If program S is executed in a state satisfying Q, then execution terminates in a state satisfying R.”

Triples like these are often called Hoare triples, after Tony Hoare, who defined them in a paper published in 1969. His notation was actually

Q{S}R

meaning “if S is executed in a state satisfying Q, then if it terminates it terminates in a state satisfying R.” This is called partial correctness; the stronger form above is called total correctness.

How can we prove things of the form {Q}S{R}? We must have, for each atomic program statement, a description of how it affects the initial state Q to produce a final state R. Then, we must have rules describing the combination of these atomic statements with sequencing operations, looping constructs, etc.

We describe the connection between Q and R for a program statement S by defining a predicate wp(S, R), called the weakest precondition of S with respect to R. Given a program S and a result state R, wp(S, R) is a predicate describing all states in which execution of S terminates in a state satisfying R. If we have a definition of wp(S, R), then we have that

{Q}S{R} iff wp(S, R) → Q.

This gives us a method for proving {Q}S{R}.

Defining wp

We’ll look at a few examples of the definition of wp for a Pascal-like language, then see how this is used to prove a program correct.

Assignment

An assignment statement looks like

x := e

where x is a program variable and e is an expression. We assume that evaluation of e does not have any side effects – the only effect of this statement is to set x to the value produced by evaluating e. The weakest precondition of an assignment is as follows:

wp(“x := e′′, R) = R[x := e]

That is, wp(“x := e′′, R) is R with x replaced by e. For example,

wp(“x := 5′′, x = 5) = (5 = 5) = true

Thus, in any state satisfying true (that is, in all states), executing “x:=5” terminates and the resulting state satisfies x = 5.

Composition

We create a statement from a sequence of statements by linking them with a semicolon (;). The weakest precondition of this compound statement depends on the weakest precondition of the component statements:

wp(“S1; S2′′, R) = wp(S1, wp(S2, R))

We can illustrate this with a program which swaps the values of the variables x and y. To describe this, we need to have a way of describing the values of the variables as well as the variables themselves. We will use capital letters for this, so that the program S satisfies

{x = X ∧ y = Y }S{x = Y ∧ y = X}

where X and Y are the initial values of x and y.

The program is

t := x; x := y; y := t,

and the condition we want to satisfy is {x = Y ∧ y = X}. So we compute:

wp(“t := x; x := y; y := t′′, x = Y ∧ y = X)
= wp(“t := x; x := y′′, wp(“y := t′′, x = Y ∧ y = X))
= wp(“t := x; x := y′′, x = Y ∧ t = X)
= wp(“t := x′′, wp(“x := y′′, x = Y ∧ t = X))
= wp(“t := x′′, y = Y ∧ t = X)
= y = Y ∧ x = X

and the result is as expected.

This proof is hard to read – it’s easier if we write it

{y = Y ∧ x = X}
t := x;
{y = Y ∧ t = X}
x := y;
{x = Y ∧ t = X}
y := t
{x = Y ∧ y = X}

This describes the states at intermediate stages, which is helpful.

Loops

Reasoning about loops is quite difficult, since we must establish termination as well as correctness. The definition of the weakest precondition of a loop is somewhat involved, so we will make use of a theorem which gives an alternative way of showing when

{Q}S{R}

is true for S a loop.

First, we must describe the syntax of a loop. A loop looks like

do B_{1} → S_{1} ; | B_{2} → S_{2} ; ⋮ ; | B_{n} → S_{n} ; od

where the B_{i} are boolean expressions which “guard” the execution of the statements S_{i}. The loop is executed by repeatedly choosing a guard B_{i} which is true, then executing the associated S_{i}. A plain loop like a while loop is just

\begin{matrix}do & B → S \\ od \end{matrix}

so that while B is true, S is executed.

To prove a statement like {Q}

do B_{1} → S_{1} ; | B_{2} → S_{2} ; ⋮ ; | B_{n} → S_{n} ; od

{R}

we need to add some information. We add a predicate P, called the loop invariant, which is true before and after each iteration of the loop, and a bound function t which is an upper bound on the number of iterations to be performed. Each iteration of the loop should decrease t by at least one. Finally, we let BB be the disjunction of all the B_{i}, so that when the loop terminates we will have ¬BB.

Now we write {Q} {inv P } {bound t}

do B_{1} → S_{1} ; | B_{2} → S_{2} ; ⋮ ; | B_{n} → S_{n} ; od

{R}

To show R holds after the loop is executed, we must show the following things:

1. P is true before execution begins.

2. {P ∧ B_{i}}S_{i}{P } for 1 ≤ i ≤ n. (That is, P is re-established after execution of S_{i}.)

3. (P ∧ ¬BB) ⇒ R.

4. (P ∧ BB) ⇒ (t > 0).

5. {P ∧ B_{i}}t1 := t; S_{i}{t < t1}, so that each iteration reduces t.

The most difficult part of this construction is finding the right loop invariant P.

Here are a couple of examples. The first example is our old pal, the integer square root.

{0 ≤ n} a := 0 {inv P: 0 ≤ a^{2} ≤ n} {bound t: n − a}

\begin{matrix}do & (a + 1)^{2} ≤ n → a := a + 1 \\ od \end{matrix}

{0 ≤ a^{2} ≤ n < (a + 1)^{2}}

The loop invariant, together with the negation of (a + 1)^{2} ≤ n, prove the postcondition. A more complex example is:

{b ≥ 0}
x := a; y := b; z := 0
{inv P: (y ≥ 0) ∧ (z + x ∗ y = a ∗ b)}
{bound t: y}
do y > 0 ∧ even(y) → y := y ÷ 2; x := x + x
| odd(y) → y := y − 1; z := z + x
od
{z = a ∗ b}

This loop computes a ∗ b using the binary representation of b (stored in y) and adding the appropriate power of 2 times x. It is practically impossible to understand without the loop invariant z + x ∗ y = a ∗ b. Note that when the loop terminates, we have ¬((y > 0 ∧ even(y)) ∨ (odd(y))) and (from the invariant) y ≥ 0, which together imply y = 0. Hence, from the invariant we have z + x ∗ 0 = a ∗ b, so z = a ∗ b.

Exercise: Check the five correctness conditions for these two loops.

Classical logic and nonlocal control

This is actually a short article I wrote for a school on type theory and term rewriting.

Abstract

Nonlocal control operators were introduced to functional languages to allow programmers to guide the evaluation process more efficiently. They can also be used to implement error handlers and concurrency mechanisms such as coroutines. However, they represent a significant addition to the principles of lambda-calculus which underlie many ideas in functional programming. Furthermore, there appears to be a deep connection between classical logic and typed lambda-calculus plus nonlocal control, similar to the connection between constructive logic and typed lambda-calculus.

An important consideration in studying languages with nonlocal control operators is that they may be nonconfluent. This property can be justified both by the connection with classical logic and by applications to programming. Because of this, many proof techniques for properties such as normalization cannot be used directly. It is hoped that this paper will motivate work on such proof methods.

1 Introduction to nonlocal control

Control operators were introduced to functional languages for reasons of efficiency. The use of continuations to describe nonlocal control flow can avoid the need to unwind deep layers of recursive calls when a result is found. This mechanism can also be used for error handling. However, control operators can be used to write very complex code – they are essentially a functional goto. Reasoning about control operators has been an important area of research in functional programming.

As it happens, a type-theoretic approach to reasoning about control operators also solves another problem – how to extend the Curry-Howard isomorphism to classical logic. The question is, “Can we extract a sensible computation from a proof which uses classical reasoning?” It turns out that some nonlocal control operators can be given types of classical axioms – in particular, axioms strong enough to prove all of classical logic when added to intuitionistic logic. Furthermore, the resulting programs extracted from classical proofs actually have a sensible computational behaviour (within some limits).

One issue which arises in considering the computational content of classical proof is that a classical proof may contain more than one piece of evidence for the proposition it proves. In general, then, proof normalization should be non-confluent – it should be possible to find each piece of evidence through reduction. Similarly, nonlocal control operators can be used to implement coroutining, a basic concurrency mechanism which permits nondeterministic interleaving of computation. Thus, it is particularly interesting to study these operators in a nonconfluent setting.

1.1 Using control operators

We begin by looking at the computational meaning of call/cc, a particular nonlocal control operator used in the language Scheme. First, we’ll look at an example of the use of call/cc to increase efficiency; then we’ll give some more formal evaluation rules.

1.1.1 Example

Let us consider an example of the use of call/cc to increase the efficiency of a functional program. Suppose we wish to write a function which takes the product of all the natural numbers in a list. Using an operator for primitive recursion, such a function could be written: λnl: list nat. list rec 1

λhd:nat.λtail:list nat.λtail prod:nat (times hd tail prod)

nl

If this function is applied to a list containing 0, this function is very inefficient. A slightly more efficient version is:

λnl: list nat. list rec 1

λhd:nat.λtail:list nat.λtail prod:nat

if zero hd 0 (times hd tail prod) nl

This version of the function ceases performing recursive calls when zero is encountered in the list. However, during the unwinding of the recursive calls, the computation still performs the multiplications on the stack. For example, if we apply this to a list (2 0 3 …), the term reduces as follows:

(list rec 1 (λhd:nat.λtail:list nat.λtail prod:nat

if zero hd 0 (times hd tail prod))) (2 0 3 …) ⇝(if zero 2 0

(times 2 (list rec 1 (λhd:nat.λtail:list nat.λtail prod:nat

if zero hd 0 (times hd tail prod)) (0 3 …)) )

⇝ (times 2 (list rec 1 (λhd:nat.λtail:list nat.λtail prod:nat

if zero hd 0 (times hd tail prod)) (0 3 …))) ⇝ (times 2 ( if zero 0 0

(times 0 (list rec 1 (λhd:nat.λtail:list nat.λtail prod:nat if zero hd 0 (times hd tail prod)) (3 …))) ))

⇝ (times 2 0)

This is not ideal, since the multiplication is still performed for everything leading up to the zero in the list. What we really want is to return zero immediately, as soon as we encounter it in the list. This is a nonlocal return, since we avoid unwinding back through the recursive calls. We can do this using call/cc:

λnl. call/cc (λk.list rec 1

λhd:nat. λtail:list nat. λtail prod:nat

if zero hd (k 0) (times hd tail prod)

nl)

Call/cc binds k to the current continuation, i.e. the “rest of the program”. In general, the continuation describes what the program will do with the value it is calculating. In this case, we simply want the function to return, so the continuation k returns the value to which it is applied. This will be made more formal in the rules below.

If we apply the function with call/cc to the list (2 0 3 …), the term reduces:

call/cc (λk. list rec 1 λhd:nat. λtail:list nat. λtail prod:nat

if zero hd (k 0) (times hd tail prod)

(2 0 3 …))

⇝ (list rec 1 (λhd:nat. λtail:list nat. λtail prod:nat

if zero hd (k 0) (times hd tail prod))) (2 0 3 …)

⇝(if zero 2 (k 0)

(times 2 (list rec 1 (λhd:nat. λtail:list nat. λtail prod:nat

if zero hd (k 0) (times hd tail prod)) (0 3 …)) ))

⇝ (times 2 (list rec 1 (λhd:nat.λtail:list nat.λtail prod:nat

if zero hd (k 0) (times hd tail prod)) (0 3 …)))

⇝ (times 2 ( if zero 0 (k 0)

(times 0 (list rec 1 (λhd:nat.λtail:list nat.λtail prod:nat if zero hd (k 0) (times hd tail prod)) (3 …))) ))

⇝ (times 2 (k 0)) ⇝ 0

The continuation at the point the call/cc was evaluated was empty (or, more precisely “return the value calculated”), so when k is applied to 0, 0 is returned immediately. If we had encountered this term in the course of another computation, k would have to describe the context in which this term appears; hence, one way of looking at continuations is “contexts as objects”. We formalize this idea below.

2 Terms, types, and evaluation rules

General use of call/cc in an untyped language like Scheme can lead to very confusing code. A straightforward technique for imposing some order on this chaos is to add types to the language. Accordingly, we will now consider our base language to be simply-typed λ calculus. To better explain the connection to classical logic, we will augment this language with disjoint union types and associated operators, described below.

The question now arises: What is the typing rule for call/cc? Let us examine the example usage above. We intend the expression call/cc(…) to have type nat. The argument to call/cc is of the form λk.t where t is an expression of type nat. The continuation k itself takes a nat as an argument, and in the context above k 0 must have type nat, which gives us the type

((nat → nat) → nat) → nat

for this instance of call/cc. However, since the evaluation of k 0 does not actually return locally, it may be given any type for the purpose of typechecking. In general, the type of call/cc has the pattern

((α → β) → α) → α

This is the classical axiom called Peirce’s Law; when added to constructive propositional logic, the result is full classical propositional logic. A fuller discussion of the issues involved in typing call/cc in ML can be found in [9].

Following the example of [6], we present the operational semantics as a set of rules representing the transition function of a term rewriting machine. We use their notion of a continuation point to represent the continuation object; however, since we do not fix an evaluation order, we shall use a more general notion of evaluation context (the analogous “applicative contexts” defined in [6] are defined for a particular evaluation order ). An evaluation context is a term with a hole in it, such that the hole is not within the scope of any binding operators. A program not in normal form can be split into an evaluation context and a redex. We use the notation E[R] for such a program, where E[] is the evaluation context and R is the redex. A continuation point is an evaluation context tagged with p. If E[R] is a program of type φ and R is of type α, then ⟨p, E[]⟩ is a continuation point which may be applied to any term of type α to produce a program of type φ.

The types we use are those of simply typed λ-calculus extended with a disjoint union type and associated operations. The reduction rules for terms are:

E[(λx.t)a] ↦ E[t[x := a]]
E[decide(inl(a); λu.t_{1}; λv.t_{2})] ↦ E[t_{1}[u := a]]

E[decide(inr(b); λu.t_{1}; λv.t_{2})] ↦ E[t_{2}[v := b]]
E[call/cc(λk.t)] ↦ E[t[k := ⟨p, E[]⟩]]
E[(⟨p, E_{0}[]⟩)a] ↦ E_{0}[a]

Another way of looking at this is to add an extra operator A, read abort, and consider a continuation ⟨p, E[]⟩ as a function λx.AE[x]. We then add a reduction rule:

E[AE_{0}[M]] ↦ E_{0}[M]

The abort operator throws away its context and leaves its argument as the result. This approach is perhaps easier to understand, but continuation application becomes a two step process of βreduction and A-reduction. (To be formal, β reduction involving the context E[] should be defined, but since x in E[x] cannot be in the scope of a binding operator, this is trivial.)

We do not specify how a term should be broken into redex and context, apart from the restriction that reduction should not occur within a binding operator. (This restriction can be relaxed; the important point is that continuation application should not make bound variables free.) This leads to a non-confluent calculus. The non-confluence in this case is a strength of the system, as it allows us to capture all of the information content of a classical proof. To illustrate this, we need to investigate further the computational meaning of classical reasoning.

2.1 Example: the law of the excluded middle

The law of the excluded middle, i.e. the axiom P ∨ ¬P, is often considered the essence of the difference between classical and intuitionistic logic. (In Gentzen’s sequent calculus, this is not the case – the essential difference is in the →-introduction rule on the right when there are multiple conclusions.) Describing the computational meaning of excluded middle illustrates the action of call/cc in connection with its classical typing.

Consider the following term:

t = call/cc(λk.inl(λx.k(inr(x))))

If x has type A, and k has type (¬A ∨ A) → ⊥ (where ¬A = A → ⊥, in the usual intuitionistic definition), then by using the type

(((¬A ∨ A) → ⊥) → (¬A ∨ A)) → (¬A ∨ A)

for call/cc we obtain a term of type ¬A ∨ A.

Suppose we wish to use this term to perform a case split on A. We would then evaluate call/cc(…) to obtain a term which we would expect to contain either a witness for A or a witness for ¬A. However, we do not have enough information to provide this witness. To solve this dilemma, the term t above, when evaluated, first appears to provide a witness λx.k(inr(x)) to A → ⊥. However, this term also contains the current continuation k, i.e. a description of the state of the computation at the point where this decision is made. Should the computation proceed in such a way that this witness λx.k(inr(x)) is applied to a term a of type A, the term then uses the continuation to return control to the point at which the split ¬A ∨ A was performed, and the computation continues with the newly supplied evidence for A instead of A → ⊥.

The term t of type ¬A ∨ A demonstrates that the evaluation of terms containing call/cc is generally only useful when they are in the context of a term which is expected to produce data. Although t can be evaluated on its own, it cannot be evaluated to a form which does not contain continuations. Attempting to use the evaluated form in another context would lead to a mismatch between the real context and the one existing when t was evaluated. However, when it is used in a term which produces, say, a natural number, the term performs useful computation.

The term t describes an element of a backtracking search procedure, providing an efficient method of abandoning one branch and switching to another. More complex uses of call/cc and the associated continuations allow switching between branches of a computation; in fact, call/cc can be used to implement coroutines and other concurrency primitives. An element of nondeterminism is inherent in concurrent systems; this alone is one reason to consider nondeterministic reduction strategies for languages which underpin concurrent constructs. Another justification, however, arises from the connection to classical logic present in the classical typing of call/cc.

3 Multiple evidence in classical proof

Control operators with classical types can be used to extract programs from classical proofs. Generally the simplest mechanism for this is to consider the type of the control operator as a new axiom or axiom scheme. This fits well with natural deduction and Hilbert-style proof systems. We take natural deduction for constructive propositional logic as an example, and add to it the operator call/cc typed with Peirce’s Law, as described in the previous section. We will also use the term t defined previously as a term typed by the law of the excluded middle:

t = call/cc(λk.inl(λx.k(inr(x)))) : (A → ⊥) ∨ A

Suppose we have the type N of natural numbers. (We do not use any property of the natural numbers – any inhabited type with at least two different elements would suffice for this example.) Consider the following proof in natural deduction, augmented with extract information:

\begin{aligned}⊢ t : ¬N ∨ N & \begin{matrix}{¬N, n : N ⊢ 1 : N \atop ¬N ⊢ N → N} & \begin{matrix}¬N ⊢ ¬N & ¬N ⊢ 2 : N \\ ¬N ⊢ ⊥ \end{matrix} ; ¬N ⊢ N \\ nn : ¬N ⊢ N \end{matrix} & a : N ⊢ N \\ & ⊢ decide(t; λnn.(λn.1)(nn2); λa.a) : N \end{aligned}

This is a proof of N, i.e. when evaluated it should supply evidence in the form of an element of N. Notice that, hidden inside the proof, there are two different elements of N – 1 and 2. Depending on the evaluation order, either piece of evidence may be produced. To see this, we begin with the term:

decide(call/cc(λk. inl(λx. k (inr(x)))); λnn. (λn.1)(nn 2); λa.a )

To evaluate the decide, we must evaluate call/cc(λk.inl(λx.k(inr(x)))) by capturing the continuation and substituting it for k. To avoid a confusingly large term, instead of performing the substitution, let k = λx. A[decide( x; λnn. (λn.1)(nn 2); λa.a)] , the context of the redex call/cc(λk.inl(λx.k(inr(x)))). Evaluation continues as follows:

decide(inl(λx. k(inr(x)))); λnn. (λn.1)(nn 2); λa.a ) ⇝ (λn.1)((λx. k(inr(x))) 2) ⇝ (λn.1)(k(inr(2)))

We now have two choices for a redex. Reducing the outermost application leads to the result 1; but reducing the application k(inr(2)) gives

decide(inr(2); λnn. (λn.1)(nn 2); λa.a) ⇝ (λa.a) 2 ⇝ 2

In a situation like this, the proof asserts that there is an element of a certain type, and the computation produces such an element. The precise element produced may vary, but it will always be of the correct type. There are many computational problems for which this is a perfectly sensible behaviour. For example, many NP-complete problems involve constraint satisfaction. Constraint solvers need only produce some result satisfying the constraints; any such result is a solution. Logic programming languages like Prolog operate directly on this principle.

Furthermore, it is generally expected that the computation steps of processes running concurrently are not determined by a fixed order; nondeterminism is what makes concurrency interesting (and difficult). The connection between classical logic, nonlocal control, and concurrency is still unclear, but examples like that above may lead to new ways of reasoning about nondeterministic computation, and, in particular, concurrent search strategies.

4 Previous work

Many of the results obtained about control operators use translation techniques to reduce the language with control to one without. This is a very useful technique, but generally these translations require the introduction of a fixed evaluation order on terms, losing the nonconfluence of the language and thus potentially throwing away information. Finding tools for reasoning about nonconfluent systems of this sort is essential for further work in this area.

Since the discovery of a classical typing for the control operator C by Griffin [8], foundational work has been done in expressing these computations as programs in a typed lambda calculus extended by nonlocal control operators. In his thesis [10], Murthy showed that a classical proof of a Π_{2}^{0} sentence φ can be interpreted as a program in an extended lambda calculus which meets the specification φ. He also demonstrated that translations from classical to intuitionistic logic correspond to continuation-passing style translations of programs with control operators to programs without. In [11], Murthy showed that this interpretation gives a computational meaning to Friedman’s conservative extension theorem for classical over constructive arithmetic for Π_{2}^{0} sentences (in [7]).

Barbanera and Berardi have proved a strong normalization result for a language including the control operator C in [2]. Unfortunately, they have some substantial restrictions on the types allowed in the language. The proof method they use is a non-trivial extension of the Tait-style strong normalization proof for simply-typed lambda calculus; it appears that the result of Barbanera and Berardi has taken this technique to its limit for this problem.

Other work on the computational content of classical proof has not explicitly mentioned nonlocal control [3, 12, 4], though connections with control operators exist [5]. Direct operations on classical proofs have also been studied, including cut elimination procedures in Gentzen’s sequent calculus [13, 14]. Results in this area hint at the complexity of the problem; some cut elimination procedures are strongly normalizing, while others are not.

References

[1] F. Barbanera and S. Berardi. A constructive semantic for classical logic and its use in extracting witnesses from proofs. In Proceedings of CAAP ’92, Lecture Notes in Computer Science 581. Springer Verlag, 1992.

[2] Franco Barbanera and Stefano Berardi. A strong normalization result for classical logic. Annals of Pure and Applied Logic, 76(2):99–116, 6 December 1995.

[3] Franco Barbanera and Stefano Berardi. A symmetric lambda calculus for classical program extraction. Information and Computation, 125(2):103–117, 15 March 1996.

[4] Ulrich Berger and Helmut Schwichtenberg. Program extraction from classical proofs. In D. Leivant, editor, Logic and Computational Complexity, International Workshop LCC ’94, Indianapolis, IN, USA, October 1994, volume 960 of Lecture Notes in Computer Science, pages 77–97. Springer Verlag, Berlin, Heidelberg, New York, 1995.

[5] P. de Groote. A CPS-Translation of the lambda-mu-calculus. Lecture Notes in Computer Science, 787, 1994.

[6] Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker, and Bruce Duba. A syntactic theory of sequential control. Theoretical Computer Science, 52:205–237, 1987.

[7] H. Friedman. Classically and intuitionistically provably recursive functions. In D.S. Scott and G.H. Muller, editors, Higher Set Theory, Lecture Notes in Mathematics, Vol. 669, pages 21–28. Springer-Verlag, 1978.

[8] T. Griffin. A formulas-as-types notion of control. In Proc. of the Seventeenth Annual Symp. on Principles of Programming Languages, pages 47–58, 1990.

[9] Robert Harper, Bruce F. Duba, and David Macqueen. Typing first-class continuations in ML. Journal of Functional Programming, 3(4):465–484, October 1993.

[10] C. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Cornell University, Dept. of Computer Science, 1990. (TR 89-1151).

[11] C. Murthy. An evaluation semantics for classical proofs. In Proc. of Sixth Symp. on Logic in Comp. Sci., pages 96–109. IEEE, Amsterdam, The Netherlands, 1991.

[12] M. Parigot. λμ-calculus: an algorithmic interpretation of classical natural deduction. In Proc. International Conference on Logic Programming and Automated Deduction, St. Petersburg, Russia, Lecture Notes in Computer Science, Vol. 624, pages 190–201. Springer-Verlag, 1992.

[13] J. Zucker. The correspondence between cut-elimination and normalization. Annals of Mathematical Logic, 7(1):1–112, 1974.

[14] J. Zucker. The correspondence between cut-elimination and normalization II. Annals of Mathematical Logic, 7(2):113–155, 1974.