This is page 1

Printer: Opaque this

What do Types Mean? — From Intrinsic to Extrinsic Semantics

John C. Reynolds

Copyright 2001 Springer-Verlag. All rights reserved. This is a draft of an article to appear in ”Essays on Programming Methodology”, edited by A. McIver and C. Morgan, to be published by Springer-Verlag. Copies must not be offered for sale.

ABSTRACT A definition of a typed language is said to be “intrinsic” if it assigns meanings to typings rather than arbitrary phrases, so that ill-typed phrases are meaningless. In contrast, a definition is said to be “extrinsic” if all phrases have meanings that are independent of their typings, while typings represent properties of these meanings.

For a simply typed lambda calculus, extended with integers, recursion, and conditional expressions, we give an intrinsic denotational semantics and a denotational semantics of the underlying untyped language. We then establish a logical relations theorem between these two semantics, and show that the logical relations can be “bracketed” by retractions between the domains of the two semantics. From these results, we derive an extrinsic semantics that uses partial equivalence relations.

There are two very different ways of giving denotational semantics to a programming language (or other formal language) with a nontrivial type system. In an intrinsic semantics, only phrases that satisfy typing judgements have meanings. Indeed, meanings are assigned to the typing judgements, rather than to the phrases themselves, so that a phrase that satisfies several judgements will have several meanings.

For example, consider λx. x (in a simply typed functional language). Corresponding to the typing judgement ⊢ λx. x : int → int, its intrinsic meaning is the identity function on the integers, while corresponding to the judgement ⊢ λx. x : bool → bool, its intrinsic meaning is the identity function on truth values. On the other hand, λx. x x, which does not satisfy any typing judgement, does not have any intrinsic meaning.

In contrast, in an extrinsic semantics, the meaning of each phrase is the same as it would be in a untyped language, regardless of its typing properties. In this view, a typing judgement is an assertion that the meaning of a phrase possesses some property.

For example, the extrinsic meaning of λx. x is the identity function on the universe of all values that can occur in a computation. In the simple case where integers and booleans can be regarded as members of this universe, the judgement ⊢ λx. x : int → int asserts that this function maps each integer into an integer, and the judgement ⊢ λx. x : bool → bool asserts that the same function maps each truth value into a truth value.

The terms “intrinsic” and “extrinsic” are recent coinages by the author [1, Chapter 15], but the concepts are much older. The intrinsic view is associated with Alonzo Church, and has been called “ontological” by Leivant [2]. The extrinsic view is associated with Haskell Curry, and has been called “semantical” by Leivant.

In this paper, we will consider the denotational semantics of a very simple typed call-by-name language with integers as a primitive type, functions, conditional expressions, and recursion definitions of values (but not of types). First, we will give an intrinsic semantics and an untyped semantics, which we will relate by a logical relations theorem. Then we will define embedding-retraction pairs between the domain specified for each type in the intrinsic semantics and the universal domain used in the untyped semantics, and we will show that these pairs “bracket” the logical relations. Finally, we will use this result to derive an extrinsic semantics in which each type denotes a partial equivalence relation on the universal domain.

In the course of this paper, we will use a variety of notations for functions. When f is a function, we write dom f for its domain. When ι_{1}, …, ι_{n} are distinct, we write [ f | ι_{1}: x_{1} | … | ι_{n}: x_{n}] for the function with domain dom f ∪ {ι_{1}, …, ι_{n}} that maps each ι_{k} into x_{k} and all other arguments ι′ into f ι′; in the special case where f is the empty function, we write [ ι_{1}: x_{1} | … | ι_{n}: x_{n}].

We write f ; g for the composition of functions f and g in diagrammatic order, and I_{D} for the identity function on the domain D. We assume that function application is left-associative, e.g., that f x y abbreviates (f x)y.

1 Syntax and Typing Rules

In defining the syntax and type system of our illustrative language, we will use the following metavariables, sometimes with decorations, to range over denumerably infinite sets of syntactic entities:

ι: variables (sometimes called identifiers)
p: phrases
θ: types
π: type assignments.

We write I to denote the set of all variables.

Since our language is an extension of the lambda calculus, a phrase may be a variable, an abstraction, or an application:

p ::= ι | λι. p′ | p′ p′′

In addition, there will be a fixed-point expression for defining a value by recursion, and a conditional expression that branches on whether a number is positive to choose between evaluating different subexpressions:

p ::= Y p′ | if p′ > 0 then p′′ else p′′′

Finally, as primitives, we will have typical constants and operations for integers:

p ::= 0 | 1 | 2 | ⋯ | p′ + p′′

(Additional integer operators would be treated the same way as +.) Types and type assignments can also be defined by an abstract grammar:

\begin{aligned}θ & ::= & int | θ_{1} → θ_{2} \\ π & ::= & ι_{1}: θ_{1}, …, ι_{n}: θ_{n} \end{aligned}

Here, ι_{1}: θ_{1}, …, ι_{n}: θ_{n} is a concrete representation of a type assignment that, abstractly, is the function on the set {ι_{1}, …, ι_{n}} that maps each variable ι_{k} into the type θ_{k}. This implies that ι_{1}, …, ι_{n} must be distinct, and that permuting the pairs ι_{k}: θ_{k} will not change the type assignment.

Informally, the primitive type int denotes the set of integers, while θ_{1} → θ_{2} denotes the set of functions that map values of type θ_{1} into values of type θ_{2}.

If π is a type assignment, p is a phrase, and θ is a type, then the formula π ⊢ p : θ is a typing judgement, or more briefly a typing, which is read “p has type θ under π”. The valid typing judgements are defined by inference rules. (In the first two rules, we rely on the fact that type assignments are functions on variables.)

\overline{π ⊢ ι : π ι} when ι ^{∈} dom π

\frac{[ π | ι: θ_{1} ] ⊢ p′ : θ_{2}}{π ⊢ λι. p′ : θ_{1} → θ_{2}}  \frac{π ⊢ p′ : θ_{1} → θ_{2}  π ⊢ p′′ : θ_{1}}{π ⊢ p′ p′′ : θ_{2}}

\frac{π ⊢ p′ : θ → θ}{π ⊢ Y p′ : θ}

\frac{π ⊢ p′ : int  π ⊢ p′′ : θ  π ⊢ p′′′ : θ}{π ⊢ if p′ > 0 then p′′ else p′′′ : θ}

\overline{π ⊢ n : int} when n is a numeral  \frac{π ⊢ p′ : int  π ⊢ p′′ : int}{π ⊢ p′ + p′′ : int.}

2 An Intrinsic Semantics

To give an intrinsic denotational semantics to our illustrative language, we must define the meanings of types, type assignments, and typing judgements. Specifically, we must give:

• for each type θ, a domain [[θ]] of values appropriate to θ,

• for each type assignment π, a domain [[π]]^{∗} of environments appropriate to π,

• for each valid typing judgement π ⊢ p : θ, a continuous function [[π ⊢ p : θ]] from [[π]]^{∗} to [[θ]], called the meaning of p with respect to π and θ.

We define a predomain to be a poset with least upper bounds of all increasing chains, and a domain to be a predomain with a least element, which we will denote by ⊥. (In fact, all of the domains we will use are Scott domains, i.e., nonempty partially ordered sets that are directed complete, bounded complete, algebraic, and countably based, but we will not make use of this fact.) A continuous function is one that preserves least upper bounds of all increasing chains; it is strict if it also preserves least elements.

In what follows, we will write Z for the sets of integers and Z_{⊥} for the flat domain obtained by discretely ordering the integers and then adding a least element ⊥ below them. When P is a predomain and D is a domain, we write P ⇒ D for the pointwise-ordered domain of continuous functions from P to D.

The meanings of types and type assignments are defined by induction on their structure:

Definition 2.1 For types θ and type assignments π, the domains [[θ]] and [[π]]^{∗} are such that

\begin{aligned}[[int]] & = & Z_{⊥} \\ [[θ_{1} → θ_{2}]] & = & [[θ_{1}]] ⇒ [[θ_{2}]] \\ [[ι_{1}: θ_{1}, …, ι_{n}: θ_{n}]]^{∗} & = & \{ [ ι_{1}: x_{1} | … | ι_{n}: x_{n}] | x_{1} ^{∈} [[θ_{1}]], …, x_{n} ^{∈} [[θ_{n}]]\}. \end{aligned}

(The set on the right of the final equation is a Cartesian product, indexed by the variables ι_{1}, …, ι_{n}, that becomes a domain when ordered componentwise.)

On the other hand, the meanings of typing judgements are defined by induction on the structure of proofs of these judgements. Specifically, for each inference rule, we give a semantic equation that expresses the meaning of a proof in which the final inference is an instance of that rule, in terms of the meanings of its immediate subproofs.

To write such equations succinctly, we write P(J) to denote a proof of the judgement J. For example, corresponding to the inference rule for function application,

\frac{π ⊢ p′ : θ_{1} → θ_{2} π ⊢ p′′ : θ_{1}}{π ⊢ p′ p′′ : θ_{2},}

we have the semantic equation

\begin{matrix}[ \frac{P(π ⊢ p′ : θ_{1} → θ_{2}) P(π ⊢ p′′ : θ_{1})}{π ⊢ p′ p′′ : θ_{2}} ] η \\ = [[P(π ⊢ p′ : θ_{1} → θ_{2})]]η([[P(π ⊢ p′′ : θ_{1})]]η), \end{matrix}

which asserts that the meaning of a proof of π ⊢ p′ p′′ : θ_{2} in which the final inference is an instance of the function-appplication rule, is a function that, when applied to an environment η, gives (m′ η)(m′′ η), where m′ and m′′ are the meanings of the immediate subproofs of the proof of π ⊢ p′ p′′ : θ_{2}.

Before proceeding further, we must warn the reader of a subtle complication in this way of defining semantics. For a sufficiently rich language, there may be many different proofs of the same typing judgement, and there is no a priori guarantee that these proofs will have the same meaning. If our intrinsic semantics is to make sense, so that we can take the meaning [[P(J)]] of any proof of a judgement J to be the meaning of J itself, then we must have the property of coherence:

Definition 2.2 An intrinsic semantics is said to be coherent if all proofs of the same judgement have the same meaning.

In fact, as we will see in Section 5, our intrinsic semantics is coherent.

The following are the semantic equations for the intrinsic semantics of our illustrative language:

[ \overline{π ⊢ ι : π ι} ] η = η ι

[ \frac{P([ π | ι: θ_{1} ] ⊢ p′ : θ_{2})}{π ⊢ λι. p′ : θ_{1} → θ_{2}} ] η = λx ^{∈} [[θ_{1}]]. [[P([ π | ι: θ_{1} ] ⊢ p′ : θ_{2})]][ η | ι: x]

[ \frac{P(π ⊢ p′ : θ_{1} → θ_{2}) P(π ⊢ p′′ : θ_{1})}{π ⊢ p′ p′′ : θ_{2}} ] η

= [[P(π ⊢ p′ : θ_{1} → θ_{2})]]η([[P(π ⊢ p′′ : θ_{1})]]η)

[ \frac{P(π ⊢ p′ : θ → θ)}{π ⊢ Y p′ : θ} ] η = ⨆_{n=0}^{∞}([[P(π ⊢ p′ : θ → θ)]]η)^{n}⊥

[ \frac{P(π ⊢ p′ : int)  P(π ⊢ p′′ : θ)  P(π ⊢ p′′′ : θ)}{π ⊢ if p′ > 0 then p′′ else p′′′ : θ} ] η

= \{ \begin{matrix}⊥ & when & [[P(π ⊢ p′ : int)]]η = ⊥ \\ [[P(π ⊢ p′′ : θ)]]η & when & [[P(π ⊢ p′ : int)]]η > 0 \\ [[P(π ⊢ p′′′ : θ)]]η & when & [[P(π ⊢ p′ : int)]]η ≤ 0 \end{matrix}

[ \overline{π ⊢ n : int} ] η = n

[ \frac{P(π ⊢ p′ : int) P(π ⊢ p′′ : int)}{π ⊢ p′ + p′′ : int} ] η

= [[P(π ⊢ p′ : int)]]η + [[P(π ⊢ p′′ : int)]]η.

3 An Untyped Semantics

Next, we consider the untyped semantics of our illustrative language. Here, independently of the type system, each phrase p possesses a unique meaning that is a mapping from environments to values, where environments map variables into values, and values range over a “universal” domain U:

[[p]] ^{∈} E ⇒ U where E = (I ⇒ U).

It is vital that this untyped semantics be call-by-name, and that U be rich enough to contain “representations” of all the typed values used in the intrinsic semantics of the previous section. These conditions, however, do not fully determine the untyped semantics. To be general, therefore, rather than specify a particular universal domain, we simply state properties of U that will be sufficient for our development. (In fact, these properties hold for a variety of untyped call-by-name models of our illustrative language.)

Specifically, we require the domains Z_{⊥} of integers (viewed as primitive values) and U ⇒ U of continuous functions (viewed as functional values) to be embeddable in U by pairs of continuous functions:

[figure: Z_{⊥}; U; Φ_{p}; Ψ_{p}; U ⇒ U; U,; Φ_{f}; Ψ_{f}]

where each Φ_{i}, Ψ_{i} is an embedding-retraction pair, i.e., each composition Φ_{i} ; Ψ_{i} is an identity function on the embedded domain.

Using these embedding-retraction pairs, it is straightforward to give semantic equations defining the untyped semantics of our language:

[[ι]] ε = ε ι
[[λι. p′]] ε = Φ_{f}(λy ^{∈} U. [[p′]][ ε | ι: y])
[[p′ p′′]] ε = Ψ_{f}([[p′]] ε)([[p′′]] ε)

[[Y p′]] ε = ⨆_{n=0}^{∞}(Ψ_{f}([[p′]] ε))^{n}⊥

[[if p′ > 0 then p′′ else p′′′]] ε = \{ \begin{matrix}⊥ & when & Ψ_{p}([[p′]] ε) = ⊥ \\ [[p′′]] ε & when & Ψ_{p}([[p′]] ε) > 0 \\ [[p′′′]] ε & when & Ψ_{p}([[p′]] ε) ≤ 0 \end{matrix}

[[n]]ε = Φ_{p} n
[[p′ + p′′]]ε = Φ_{p}(Ψ_{p}([[p′]]ε) + Ψ_{p}([[p′′]]ε)).

4 Logical Relations

Our next task is to connect the intrinsic and untyped semantics by means of a type-indexed family ρ of relations such that

ρ[θ] ⊆ [[θ]] × U.

The members ρ[θ] of this family are called logical relations. Informally, ⟨x, y⟩ ^{∈} ρ[θ] means that the value x of type θ is represented by the untyped value y.

(Logical relations [3] are most often used to connect two intrinsic typed semantics, but the idea works just as well to connect an intrinsic and an untyped semantics.)

The logical relations are defined by induction on the structure of types:

Definition 4.1 For types θ, the logical relations ρ[θ] ⊆ [[θ]] × U are such that:

⟨x, y⟩ ^{∈} ρ[int] iff x = Ψ_{p}y
⟨f, g⟩ ^{∈} ρ[θ_{1} → θ_{2}] iff ∀⟨x, y⟩ ^{∈} ρ[θ_{1}]. ⟨f x, Ψ_{f} g y⟩ ^{∈} ρ[θ_{2}].

To explicate the logical relations, we begin with two domain-theoretic properties that will be necessary to deal with recursion:

Definition 4.2 A relation r between domains is

• strict iff ⟨⊥, ⊥⟩ ^{∈} r,

• chain-complete iff, whenever x_{0} ⊑ x_{1} ⊑ ⋯ and y_{0} ⊑ y_{1} ⊑ ⋯ are increasing sequences such that each ⟨x_{i}, y_{i}⟩ ^{∈} r,

⟨⨆_{i=0}^{∞}x_{i}, ⨆_{i=0}^{∞}y_{i}⟩ ^{∈} r.

Lemma 4.3 For all types θ, the logical relations ρ[θ] are strict and chaincomplete.

Proof. We first note that, if Φ, Ψ is any embedding-retraction pair, then ⊥ ⊑ Φ⊥, and since Ψ is monotone (since it is continuous) and Φ ; Ψ is an identity, Ψ⊥ ⊑ Ψ(Φ⊥) = ⊥. Then since ⊥ ⊑ Ψ⊥, we have Ψ⊥ = ⊥, i.e., Ψ is a strict function.

The main proof is by induction on the structure of θ.

• Suppose θ is int. Since Ψ_{p} is strict, we have ⊥ = Ψ_{p}⊥, so that ⟨⊥, ⊥⟩ ^{∈} ρ[int].

Now suppose that x_{i} and y_{i} are increasing sequences, in Z_{⊥} and U respectively, such that ⟨x_{i}, y_{i}⟩ ^{∈} ρ[int]. Then x_{i} = Ψ_{p}y_{i} for i ≥ 0, so that ⨆_{i=0}^{∞}x_{i} = ⨆_{i=0}^{∞}Ψ_{p}y_{i}, and since Ψ_{p} is continuous, ⨆_{i=0}^{∞}x_{i} = Ψ_{p}(⨆_{i=0}^{∞}y_{i}). Thus ⟨⨆_{i=0}^{∞}x_{i}, ⨆_{i=0}^{∞}y_{i}⟩ ^{∈} ρ[int].

• Suppose θ is θ_{1} → θ_{2}. Let f = ⊥ and g = ⊥, so that Ψ_{f} g = ⊥, since Ψ_{f} is strict. Then, for any ⟨x, y⟩ ^{∈} ρ[θ_{1}], since the least element of a domain of functions is the constant function yielding ⊥, f x = ⊥ and Ψ_{f} g y = ⊥. By the induction hypothesis for θ_{2}, ⟨f x, Ψ_{f} g y⟩ = ⟨⊥, ⊥⟩ ^{∈} ρ[θ_{2}], and since this holds for all ⟨x, y⟩ ^{∈} ρ[θ_{1}], we have ⟨f, g⟩ = ⟨⊥, ⊥⟩ ^{∈} ρ[θ_{1} → θ_{2}].

Now suppose that f_{i} and g_{i} are increasing sequences, in [[θ_{1} → θ_{2}]] and U respectively, such that ⟨f_{i}, g_{i}⟩ ^{∈} ρ[θ_{1} → θ_{2}]. Let ⟨x, y⟩ ^{∈} ρ[θ_{1}]. Then ⟨f_{i} x, Ψ_{f} g_{i} y⟩ ^{∈} ρ[θ_{2}] for i ≥ 0, and since function application and Ψ_{f} are monotone, f_{i} x and Ψ_{f} g_{i} y are increasing sequences. Then, since Ψ_{f} is continuous, and a least upper bound of functions distributes through application, the induction hypothesis for θ_{2} gives

⟨(⨆_{i=0}^{∞}f_{i})x, Ψ_{f}(⨆_{i=0}^{∞}g_{i})y⟩ = ⟨⨆_{i=0}^{∞}f_{i} x, ⨆_{i=0}^{∞}Ψ_{f} g_{i} y⟩ ^{∈} ρ[θ_{2}],

and since this holds for all ⟨x, y⟩ ^{∈} ρ[θ_{1}], we have ⟨⨆_{i=0}^{∞}f_{i}, ⨆_{i=0}^{∞}g_{i}⟩ ^{∈} ρ[θ_{1} → θ_{2}].

end of proof

Now we can establish our central result. Essentially, it asserts that, in related environments, the typed and untyped meanings of the same expression give related values, where the type-dependent notion of “related” is given by the logical relations:

Theorem 4.4 (The Logical Relations Theorem) Suppose P(π ⊢ p : θ) is a proof of the typing judgement π ⊢ p : θ, and

\begin{matrix}∀ι ^{∈} dom π. η ι ^{∈} [[π ι]] \\ ε ^{∈} I ⇒ U \\ ∀ι ^{∈} dom π. ⟨η ι, ε ι⟩ ^{∈} ρ[π ι], \end{matrix}  (A)

Then

⟨[[P(π ⊢ p : θ)]]η, [[p]]ε⟩ ^{∈} ρ[θ]. (B)

Proof. By induction on the structure of the proof P(π ⊢ p : θ). More precisely, we prove by induction on n that, for all π, η, ε, p, θ, and P(π ⊢ p : θ), if the depth of P(π ⊢ p : θ) is at most n, and the assumptions (A) hold, then (B) holds. However, in all of the following cases except that for abstractions (i.e., λι. p), the induction hypotheses are only applied for the same values of π, η, and ε as in the theorem being proved. (Abstractions are the only exception because they are the only binding construction in our language.)

• Suppose P(π ⊢ p : θ) is

\overline{π ⊢ ι : π ι,}

so that

\begin{aligned}[[P(π ⊢ p : θ)]]η & = & η ι \\ [[p]]ε & = & ε ι. \end{aligned}

Assume (A). Then

⟨[[P(π ⊢ p : θ)]]η, [[p]]ε⟩ = ⟨η ι, ε ι⟩ ^{∈} ρ[π ι] = ρ[θ].

• Suppose P(π ⊢ p : θ) is

\frac{P([ π | ι: θ_{1} ] ⊢ p′ : θ_{2})}{π ⊢ λι. p′ : θ_{1} → θ_{2},}

so that

\begin{aligned}[[P(π ⊢ p : θ)]]η & = & λx ^{∈} [[θ_{1}]]. [[P([ π | ι: θ_{1} ] ⊢ p′ : θ_{2})]][ η | ι: x] \\ [[p]]ε & = & Φ_{f}(λy ^{∈} U. [[p′]][ ε | ι: y]). \end{aligned}

Assume (A), and suppose ⟨x, y⟩ ^{∈} ρ[θ_{1}]. Then

\begin{matrix}∀ι′ ^{∈} dom[ π | ι: θ_{1} ]. [ η | ι: x] ι′ ^{∈} [[[ π | ι: θ_{1} ] ι′]] \\ [ ε | ι: y] ^{∈} I ⇒ U \\ ∀ι′ ^{∈} dom[ π | ι: θ_{1} ]. ⟨[ η | ι: x] ι′, [ ε | ι: y] ι′⟩ ^{∈} ρ[[ π | ι: θ_{1} ] ι′], \end{matrix}(A′)

so that

⟨[[P(π ⊢ p : θ)]]η x, Ψ_{f}([[p]]ε) y⟩

= ⟨[[P([ π | ι: θ_{1} ] ⊢ p′ : θ_{2})]][ η | ι: x], Ψ_{f}(Φ_{f}(λy. [[p′]][ ε | ι: y]))y⟩

= ⟨[[P([ π | ι: θ_{1} ] ⊢ p′ : θ_{2})]][ η | ι: x], [[p′]][ ε | ι: y]⟩
∈ ρ[θ_{2}],

where the last step follows from the induction hypothesis for P([ π | ι: θ_{1} ] ⊢ p′ : θ_{2}), taking (A) to be (A′). Then, since this holds for all ⟨x, y⟩ ^{∈} ρ[θ_{1}], the definition (4.1) of ρ[θ_{1} → θ_{2}] gives

⟨[[P(π ⊢ p : θ)]]η, [[p]]ε⟩ ^{∈} ρ[θ_{1} → θ_{2}].

• Suppose P(π ⊢ p : θ) is

\frac{P(π ⊢ p′ : θ_{1} → θ_{2}) P(π ⊢ p′′ : θ_{1})}{π ⊢ p′ p′′ : θ_{2},}

so that

\begin{aligned}[[P(π ⊢ p : θ)]]η & = & [[P(π ⊢ p′ : θ_{1} → θ_{2})]]η([[P(π ⊢ p′′ : θ_{1})]]η) \\ [[p]]ε & = & Ψ_{f}([[p′]] ε)([[p′′]] ε). \end{aligned}

Assume (A). Then the induction hypothesis for P(π ⊢ p′ : θ_{1} → θ_{2}) gives

⟨[[P(π ⊢ p′ : θ_{1} → θ_{2})]]η, [[p′]] ε⟩ ^{∈} ρ[θ_{1} → θ_{2}],

and the induction hypothesis for P(π ⊢ p′′ : θ_{1}) gives

⟨[[P(π ⊢ p′′ : θ_{1})]]η, [[p′′]] ε⟩ ^{∈} ρ[θ_{1}],

so that

⟨[[P(π ⊢ p : θ)]]η, [[p]]ε⟩

= ⟨[[P(π ⊢ p′ : θ_{1} → θ_{2})]]η([[P(π ⊢ p′′ : θ_{1})]]η), Ψ_{f}([[p′]]ε)([[p′′]]ε)⟩

∈ ρ[θ_{2}],

by the definition (4.1) of ρ[θ_{1} → θ_{2}].

• Suppose P(π ⊢ p : θ) is

\frac{P(π ⊢ p′ : θ → θ)}{π ⊢ Y p′ : θ.,}

so that

\begin{aligned}[[P(π ⊢ p : θ)]]η & = & ⨆_{n=0}^{∞}([[P(π ⊢ p′ : θ → θ)]]η)^{n}⊥ \\ [[p]]ε & = & ⨆_{n=0}^{∞}(Ψ_{f}([[p′]] ε))^{n}⊥. \end{aligned}

Assume (A). By the induction hypothesis, we have

⟨[[P(π ⊢ p′ : θ → θ)]]η, [[p′]] ε⟩ ^{∈} ρ[θ → θ].

Next we can show, by induction on n, that

⟨([[P(π ⊢ p′ : θ → θ)]]η)^{n}⊥,(Ψ_{f}([[p′]] ε))^{n}⊥⟩^{∈} ρ[θ]. The case for n = 0 follows since, by Lemma 4.3, ρ[θ] is strict. For the induction step, we have

⟨([[P(π ⊢ p′ : θ → θ)]]η)^{n+1}⊥,(Ψ_{f}([[p′]] ε))^{n+1}⊥⟩

= ⟨[[P(π ⊢ p′ : θ → θ)]]η(([[P(π ⊢ p′ : θ → θ)]]η)^{n}⊥),
Ψ_{f}([[p′]] ε)((Ψ_{f}([[p′]] ε))^{n}⊥)⟩
∈ ρ[θ],

by the induction hypothesis for n and the definition (4.1) of ρ[θ → θ]. Finally,

⟨[[P(π ⊢ p : θ)]]η, [[p]]ε⟩

= ⟨ ⨆_{n=0}^{∞}([[P(π ⊢ p′ : θ → θ)]]η)^{n}⊥, ⨆_{n=0}^{∞}(Ψ_{f}([[p′]] ε))^{n}⊥⟩

∈ ρ[θ],

since ρ[θ] is chain-complete by Lemma 4.3.

• Suppose P(π ⊢ p : θ) is

\frac{P(π ⊢ p′ : int)  P(π ⊢ p′′ : θ)  P(π ⊢ p′′′ : θ)}{π ⊢ if p′ > 0 then p′′ else p′′′ : θ,}

so that

[[P(π ⊢ p: θ)]]η = \{ \begin{matrix}⊥ & when & [[P(π ⊢ p′: int)]]η = ⊥ \\ [[P(π ⊢ p′′: θ)]]η & when & [[P(π ⊢ p′: int)]]η > 0 \\ [[P(π ⊢ p′′′: θ)]]η & when & [[P(π ⊢ p′: int)]]η ≤ 0 \end{matrix}

[[p]]ε = \{ \begin{matrix}⊥ & when & Ψ_{p}([[p′]] ε) = ⊥ \\ [[p′′]] ε & when & Ψ_{p}([[p′]] ε) > 0 \\ [[p′′′]] ε & when & Ψ_{p}([[p′]] ε) ≤ 0. \end{matrix}

Assume (A). By the induction hypothesis for P(π ⊢ p′ : int),

⟨[[P(π ⊢ p′ : int)]]η, [[p′]]ε⟩ ^{∈} ρ[int],

so that [[P(π ⊢ p′ : int)]]η = Ψ_{p}([[p′]]ε). There are three cases:

– If Ψ_{p}[[p′]]ε = ⊥, then

⟨[[P(π ⊢ p: θ)]]η, [[p]]ε⟩ = ⟨⊥, ⊥⟩,

which belongs to ρ[θ] since ρ[θ] is strict.

– If Ψ_{p}[[p′]]ε > 0, then

⟨[[P(π ⊢ p: θ)]]η, [[p]]ε⟩ = ⟨[[P(π ⊢ p′′: θ)]]η, [[p′′]]ε⟩,

which belongs to ρ[θ] by the induction hypothesis for P(π ⊢ p′′: θ).

– If Ψ_{p}[[p′]]ε ≤ 0, then

⟨[[P(π ⊢ p: θ)]]η, [[p]]ε⟩ = ⟨[[P(π ⊢ p′′′: θ)]]η, [[p′′′]]ε⟩,

which belongs to ρ[θ] by the induction hypothesis for P(π ⊢ p′′′: θ).

• Suppose P(π ⊢ p : θ) is

\overline{π ⊢ n : int,}

so that

\begin{aligned}[[P(π ⊢ p : θ)]]η & = & n \\ [[p]]ε & = & Φ_{p} n. \end{aligned}

Then, since Φ_{p} ; Ψ_{p} is an identity, [[P(π ⊢ p : θ)]]η = Ψ_{p}(Φ_{p} n) = Ψ_{p}([[p]]ε), so that

⟨[[P(π ⊢ p : θ)]]η, [[p]]ε⟩ ^{∈} ρ[int].

• Suppose P(π ⊢ p : θ) is

\frac{P(π ⊢ p′ : int) P(π ⊢ p′′ : int)}{π ⊢ p′ + p′′ : int,}

so that

[[P(π ⊢ p : θ)]]η = [[P(π ⊢ p′ : int)]]η + [[P(π ⊢ p′′ : int)]]η
[[p]]ε = Φ_{p}(Ψ_{p}([[p′]]ε) + Ψ_{p}([[p′′]]ε)).

Assume (A). By the induction hypothesis for P(π ⊢ p′ : int), we have

[[P(π ⊢ p′ : int)]]η = Ψ_{p}([[p′]]ε),

and a similar argument holds for p′′. Then

[[P(π ⊢ p : θ)]]η = Ψ_{p}([[p′]]ε) + Ψ_{p}([[p′′]]ε)
= Ψ_{p}(Φ_{p}(Ψ_{p}([[p′]]ε) + Ψ_{p}([[p′′]]ε)))
= Ψ_{p}([[p]]ε),

since Φ_{p} ; Ψ_{p} is an identity. Thus

⟨[[P(π ⊢ p : θ)]]η, [[p]]ε⟩ ^{∈} ρ[int].

end of proof

5 Bracketing

Next, we show that the domains [[θ]] that are the meanings of types can be embedded in the universal domain U by a type-indexed family of function pairs:

[figure: [[θ]]; U.; ϕ[θ]; ψ[θ]]

We will show that these are embedding-retraction pairs, and that they are closely related to the logical relations defined in the previous section. (The idea that types denote retractions on a universal domain is due to Scott [4].)

Definition 5.1 For types θ, the functions ϕ[θ] ^{∈} [[θ]] → U and ψ[θ] ^{∈} U → [[θ]] are such that

ϕ[int]x = Φ_{p} x
ψ[int]y = Ψ_{p} y
ϕ[θ_{1} → θ_{2}]f = Φ_{f}(ψ[θ_{1}] ; f ; ϕ[θ_{2}])
ψ[θ_{1} → θ_{2}]y = ϕ[θ_{1}] ; Ψ_{f}y ; ψ[θ_{2}].

These function pairs are related to the logical relations ρ[θ] by the following theorem:

Theorem 5.2 (The Bracketing Theorem) For each type θ:

1. For all x ^{∈} [[θ]], ⟨x, ϕ[θ]x⟩ ^{∈} ρ[θ].

2. For all ⟨x, y⟩ ^{∈} ρ[θ], x = ψ[θ]y.

Proof. The proof is by induction on the structure of θ:

• Suppose θ is int and x ^{∈} [[int]]. From the fact that Φ_{p} ; Ψ_{p} is an identity, and the definition (5.1) of ϕ[int], we have x = Ψ_{p}(Φ_{p} x) = Ψ_{p}(ϕ[int]x). Then the definition (4.1) of ρ[int] gives ⟨x, ϕ[int]x⟩ ^{∈} ρ[int].

Now suppose ⟨x, y⟩ ^{∈} ρ[int]. Then the definitions (4.1) of ρ[int] and (5.1) of ψ[int] give x = Ψ_{p} y = ψ[int]y.

• Suppose θ is θ_{1} → θ_{2}, and f ^{∈} [[θ_{1} → θ_{2}]]. Let ⟨x, y⟩ ^{∈} ρ[θ_{1}]. By the second part of the induction hypothesis for θ_{1}, x = ψ[θ_{1}]y. Then

ϕ[θ_{2}](f x) = ϕ[θ_{2}](f(ψ[θ_{1}]y))
= (ψ[θ_{1}] ; f ; ϕ[θ_{2}])y
= Ψ_{f}(Φ_{f}(ψ[θ_{1}] ; f ; ϕ[θ_{2}]))y
= Ψ_{f}(ϕ[θ_{1} → θ_{2}]f)y,

from the fact that Φ_{f} ; Ψ_{f} is an identity, and the definition (5.1) of ϕ[θ_{1} → θ_{2}]. Then by the first part of the induction hypothesis for θ_{2},

⟨f x, Ψ_{f}(ϕ[θ_{1} → θ_{2}]f)y⟩ ^{∈} ρ[θ_{2}],

and since this holds for all ⟨x, y⟩ ^{∈} ρ[θ_{1}], the definition (4.1) of ρ[θ_{1} → θ_{2}] gives

⟨f, ϕ[θ_{1} → θ_{2}]f⟩ ^{∈} ρ[θ_{1} → θ_{2}].

Now suppose ⟨f, g⟩ ^{∈} ρ[θ_{1} → θ_{2}], and let x ^{∈} [[θ_{1}]]. By the first part of the induction hypothesis for θ_{1}, ⟨x, ϕ[θ_{1}]x⟩ ^{∈} ρ[θ_{1}], so by the definition (4.1) of ρ[θ_{1} → θ_{2}], ⟨f x, Ψ_{f}g(ϕ[θ_{1}]x)⟩ ^{∈} ρ[θ_{2}]. Then by the second part of the induction hypothesis for θ_{2}, f x = ψ[θ_{2}](Ψ_{f}g(ϕ[θ_{1}]x)).

Since this holds for all x ^{∈} [[θ_{1}]], we have f = ϕ[θ_{1}] ; Ψ_{f}g ; ψ[θ_{2}], and by the definition (5.1) of ψ[θ_{1} → θ_{2}], f = ψ[θ_{1} → θ_{2}]g.

end of proof

An immediate consequence of the bracketing theorem is that

Corollary 5.3 The ϕ[θ], ψ[θ] are embedding-retraction pairs.

Proof. Suppose x ^{∈} [[θ]]. By the first part of the bracketing theorem, ⟨x, ϕ[θ]x⟩ ^{∈} ρ[θ]; then by the second part, x = ψ[θ](ϕ[θ]x). Since this holds for all x ^{∈} [[θ]], we have ϕ[θ] ; ψ[θ] = I_{[[θ]]}. end of proof

The name “bracketing theorem” alludes to a more succinct formulation of the theorem as a subset relationship between graphs of functions and relations. Writing † for the reflection of a graph, we can restate the bracketing theorem as:

For each type θ, ϕ[θ] ⊆ ρ[θ] ⊆ (ψ[θ])^{†}.

The essence of the bracketing theorem is that it connects the notion of representation provided by the logical relations with the different notion provided by the embedding-retraction pairs. For each typed value x ^{∈} [[θ]], one can regard

• the set { y | x = ψ[θ]y } (i.e., the preimage of x under ψ[θ]) as the set of untyped values that “weakly” represent x,

• the subset { y | ⟨x, y⟩ ^{∈} ρ[θ] } ⊆ { y | x = ψ[θ]y } as the set of untyped values that represent x,

• the member ϕ[θ]x ^{∈} { y | ⟨x, y⟩ ^{∈} ρ[θ] } as the “best” or “canonical” representation of x.

An essential difference between representation and weak representation is that, since ψ[θ] is a total function, every untyped value “weakly” represents some typed value.

By combining the bracketing theorem with the logical relations theorem, one can express the intrinsic typed semantics of a phrase in terms of its untyped semantics:

Theorem 5.4 Suppose π ⊢ p : θ and η ^{∈} [[π]]^{∗}. Then

[[P(π ⊢ p : θ)]]η = ψ[θ]([[p]](λι. if ι ^{∈} dom π then ϕ[π ι](η ι) else ⊥)).

Proof. Let ε = λι. if ι ^{∈} dom π then ϕ[π ι](η ι) else ⊥. For each ι ^{∈} dom π, by this definition of ε and the first part of the bracketing theorem,

⟨η ι, ε ι⟩ = ⟨η ι, ϕ[π ι](η ι)⟩ ^{∈} ρ[π ι].

Then the logical relations theorem gives

⟨[[P(π ⊢ p : θ)]]η, [[p]]ε⟩ ^{∈} ρ[θ],

and the second part of the bracketing theorem gives

[[P(π ⊢ p : θ)]]η = ψ[θ]([[p]]ε).

end of proof

Theorem 5.4 expresses the meaning of a proof of the typing judgement π ⊢ p : θ in terms of the untyped meaning of p and the retractionembedding pairs associated with θ and the components of π — all of which are determined by the judgement itself rather than its proof. Thus every proof of the same judgement must have the same intrinsic semantics:

Corollary 5.5 The intrinsic semantics is coherent.

In fact, the coherence of the simple kind of language we have been considering here has long been known, but we believe this is an unusually elegant proof.

It should also be noted that the above theorem expresses a particular intrinsic semantics in terms of any of a variety of untyped semantics, i.e., all of the untyped semantics meeting the constraints in Section 3, where we permitted variations in the universal domain U and the way in which integers and functions are embedded within it.

For example, one might take the untyped semantics to be one in which η-reduction does or does not preserve meaning [1, Section 10.5], or one in which the fixed-point combinator λf. (λx. f(x x))(λx. f(x x)) is or is not a least fixed-point operator [5].

6 An Extrinsic PER Semantics

Suppose we define a type-indexed family of relations between untyped values:

Definition 6.1 For types θ, the relations σ[θ] ⊆ U × U are such that

⟨y, y′⟩ ^{∈} σ[θ] iff ∃x ^{∈} [[θ]]. ⟨x, y⟩, ⟨x, y′⟩ ^{∈} ρ[θ].

(More abstractly, using relational composition, σ[θ] =^{def} (ρ[θ])^{†} ; ρ[θ].)

Obviously, the σ[θ] are symmetric. Moreover, these relations are transitive:

Theorem 6.2 If ⟨y, y′⟩, ⟨y′, y′′⟩ ^{∈} σ[θ], then ⟨y, y′′⟩ ^{∈} σ[θ].

Proof. If ⟨y, y′⟩, ⟨y′, y′′⟩ ^{∈} σ[θ], then there are x, x′ ^{∈} [[θ]] such that ⟨x, y⟩, ⟨x, y′⟩, ⟨x′, y′⟩, ⟨x′, y′′⟩ ^{∈} ρ[θ]. Then by the second part of the bracketing theorem, x = ψ[θ]y′ and x′ = ψ[θ]y′, so that x = x′. Then ⟨x, y⟩, ⟨x, y′′⟩ ^{∈} ρ[θ], so that ⟨y, y′′⟩ ^{∈} σ[θ]. end of proof

Thus, the σ[θ] are partial equivalence relations (PER’s). Although we have chosen to define them in terms of the logical relations, they can also be described directly by induction on the structure of θ:

Theorem 6.3

⟨y, y′⟩ ^{∈} σ[int] iff Ψ_{p}y = Ψ_{p}y′
⟨g, g′⟩ ^{∈} σ[θ_{1} → θ_{2}] iff ∀⟨y, y′⟩ ^{∈} σ[θ_{1}]. ⟨Ψ_{f} g y, Ψ_{f} g′ y′⟩ ^{∈} σ[θ_{2}].

Proof. Using the definitions (6.1) of σ, and (4.1) of ρ[int], we have ⟨y, y′⟩ ^{∈} σ[int] iff there is an x ^{∈} [[int]] such that ⟨x, y⟩, ⟨x, y′⟩ ^{∈} ρ[int], iff there is an x ^{∈} [[int]] such that x = Ψ_{p} y and x = Ψ_{p} y′, iff Ψ_{p} y = Ψ_{p} y′.

Suppose ⟨g, g′⟩ ^{∈} σ[θ_{1} → θ_{2}] and ⟨y, y′⟩ ^{∈} σ[θ_{1}]. From the definition (6.1) of σ, there is an f ^{∈} [[θ_{1} → θ_{2}]] such that ⟨f, g⟩, ⟨f, g′⟩ ^{∈} ρ[θ_{1} → θ_{2}] and there is an x ^{∈} [[θ_{1}]] such that ⟨x, y⟩, ⟨x, y′⟩ ^{∈} ρ[θ_{1}]. Then, from the definition (4.1) of ρ[θ_{1} → θ_{2}], we have ⟨f x, Ψ_{f} g y⟩ ^{∈} ρ[θ_{2}] and ⟨f x, Ψ_{f} g′ y′⟩ ^{∈} ρ[θ_{2}], and from the definition (6.1) of σ, we have ⟨Ψ_{f} g y, Ψ_{f} g′ y′⟩ ^{∈} σ[θ_{2}].

On the other hand, suppose

∀⟨y, y′⟩ ^{∈} σ[θ_{1}]. ⟨Ψ_{f} g y, Ψ_{f} g′ y′⟩ ^{∈} σ[θ_{2}],

and let ⟨x, y⟩ ^{∈} ρ[θ_{1}]. We have ⟨y, y⟩ ^{∈} σ[θ_{1}] by the definition (6.1) of σ. Moreover, since the first half of the bracketing theorem gives ⟨x, ϕ[θ_{1}]x⟩ ^{∈} ρ[θ_{1}], we also have ⟨ϕ[θ_{1}]x, y⟩ ^{∈} σ[θ_{1}] by the definition (6.1) of σ. Then, by the supposition displayed above, we have both ⟨Ψ_{f} g y, Ψ_{f} g′ y⟩ ^{∈} σ[θ_{2}] and ⟨Ψ_{f} g(ϕ[θ_{1}]x), Ψ_{f} g′ y⟩ ^{∈} σ[θ_{2}], and since σ[θ_{2}] is symmetric and transitive, ⟨Ψ_{f} g(ϕ[θ_{1}]x), Ψ_{f} g y⟩ ^{∈} σ[θ_{2}].

Thus we have ⟨Ψ_{f} g(ϕ[θ_{1}]x), Ψ_{f} ĝ y⟩ ^{∈} σ[θ_{2}], where ĝ is either g or g′. By the definition (6.1) of σ, there is a w ^{∈} [[θ_{2}]] such that ⟨w, Ψ_{f} g(ϕ[θ_{1}]x)⟩ ^{∈} ρ[θ_{2}] and ⟨w, Ψ_{f} ĝ y⟩ ^{∈} ρ[θ_{2}]. From the first of these inclusions, the second part of the bracketing theorem gives w = ψ[θ_{2}](Ψ_{f} g(ϕ[θ_{1}]x)), or w = f x, where f is the function ϕ[θ_{1}] ; Ψ_{f} g ; ψ[θ_{2}]. Thus the second inclusion can be written as ⟨f x, Ψ_{f} ĝ y⟩ ^{∈} ρ[θ_{2}]. Since this holds for all ⟨x, y⟩ ^{∈} ρ[θ_{1}], the definition (4.1) of ρ[θ_{1} → θ_{2}] gives ⟨f, ĝ⟩ ^{∈} ρ[θ_{1} → θ_{2}], and since this holds when ĝ is either g or g′, the definition (6.1) of σ gives ⟨g, g′⟩ ^{∈} σ[θ_{1} → θ_{2}].

end of proof

In terms of the notion of representation captured by the logical relations:

• ⟨y, y⟩ ^{∈} σ[θ] means that y is a representation of some value of type θ.

• ⟨y, y′⟩ ^{∈} σ[θ] means that y and y′ are representions of the same value of type θ.

Thus, for each θ, the PER σ[θ] defines both the set { y | ⟨y, y⟩ ^{∈} σ[θ] } of “representations” and also, when restricted to this set, an equivalence relation of “representing the same thing”.

In early extrinsic denotational semantics, such as the Sethi-MacQueen model [7, 8], types played only the first of these roles; the insight that they denote PER’s (rather than subsets) on a universal domain of untyped values is due to Scott [4, Section 7], [9, Section 5], [10].

In fact, the basic idea that types represent equivalence relations on subsets of some universe of “realizers” is much older. Two examples are described by Troelstra: the “hereditarily effective operations” (HEO) [11, Section 2.4.11], [12, Section 3.3], where the realizers are natural numbers (used as Gödel numbers), and the “extensional model of hereditarily continuous functionals” (ECF) [11, Section 2.6.5], [12, Section 3.9], where the realizers are functions from natural numbers to natural numbers. Troelstra attributes HEO to Kreisel [13, Section 4.2], and ECF to both Kreisel [13] and, independently, Kleene [14].

The common thread behind all these systems is that, to be continuous (or computable) a typed value must be represented by some realizer. An overview of realizability is given by Amadio and Curien [15, Chapter 15].

The combination of our untyped semantics with the PER’s σ[θ] gives what we have called an extrinsic semantics. The essential connection between these entities is that, when a phrase satisfies a typing judgement, its untyped meaning respects the type-dependent notion of representation described by the σ[θ]. More precisely,

Theorem 6.4 Suppose π ⊢ p : θ, and ε, ε′ ^{∈} I ⇒ U satisfy

∀ι ^{∈} dom π. ⟨ε ι, ε′ ι⟩ ^{∈} σ[π ι].

Then

⟨[[p]]ε, [[p]]ε′⟩ ^{∈} σ[θ].

Proof. If ε and ε′ are related as supposed, then for each ι ^{∈} dom π, there must be an x ^{∈} [[π ι]] such that ⟨x, ε ι⟩, ⟨x, ε′ ι⟩ ^{∈} ρ[π ι]. Thus there must be an environment η ^{∈} [[π]]^{∗} such that

∀ι ^{∈} dom π. ⟨η ι, ε ι⟩, ⟨η ι, ε′ ι⟩ ^{∈} ρ[π ι].

Then by two applications of the logical relations theorem,

⟨[[P(π ⊢ p : θ)]]η, [[p]]ε⟩, ⟨[[P(π ⊢ p : θ)]]η, [[p]]ε′⟩ ^{∈} ρ[θ],

so that

⟨[[p]]ε, [[p]]ε′⟩ ^{∈} σ[θ].

end of proof

7 Further Work and Future Directions

The development we have presented here extends in a straightforward manner to a richer programming language that includes several primitive types, subtyping, and named products (with field-forgetting implicit conversions)

[16]. (Some additional properties of ρ[θ] and σ[θ] are also proved in this reference.)

Obviously, we would like to treat still richer type systems, such as intersection or polymorphic types. During the last year, we made a strenuous attempt to conquer intersection types, but we were unable to find a semantics for which we could prove the bracketing theorem. (This work was described in a talk at the Workshop on Intersection Types and Related Systems [17].)

It is also of interest to try to move in the opposite direction, from extrinsic to intrinsic semantics. In a sense this is straightforward: Given σ[θ], one simply takes [[θ]] to be the set of equivalence classes of σ[θ]. (More precisely, one takes the semantic category to be a category of PER’s [15, Chapter 15].) In general, however, there may be no sensible way to order the set of equivalence classes to make [[θ]] into a domain.

8 Acknowledgements

This research was supported in part by National Science Foundation Grant CCR-9804014. Much of the research was carried out during two delightful and productive visits to BRICS^{1} in Aarhus, Denmark, September to November 1999 and May to June 2000.

9 References

[1] John C. Reynolds. Theories of Programming Languages. Cambridge University Press, Cambridge, England, 1998.

[2] Daniel Leivant. Typing and computational properties of lambda expressions. Theoretical Computer Science, 44(1):51–68, 1986.

[3] Gordon D. Plotkin. Lambda-definability and logical relations. Memorandum SAI–RM–4, University of Edinburgh, Edinburgh, Scotland, October 1973.

[4] Dana S. Scott. Data types as lattices. SIAM Journal on Computing, 5(3):522–587, September 1976.

[5] David M. R. Park. The Y-combinator in Scott’s lambda-calculus models. Symposium on Theory of Programming, University of Warwick, unpublished; cited in [6], 1970.

1

Basic Research in Computer Science (http://www.brics.dk/),

Centre of the Danish National Research Foundation.

[6] Christopher P. Wadsworth. The relation between computational and denotational properties for Scott’s D_{∞}-models of the lambda-calculus. SIAM Journal on Computing, 5(3):488–521, September 1976.

[7] David B. MacQueen and Ravi Sethi. A semantic model of types for applicative languages. In Conference Record of the 1982 ACM Symposium on LISP and Functional Programming, pages 243–252, New York, 1982. ACM.

[8] David B. MacQueen, Gordon D. Plotkin, and Ravi Sethi. An ideal model for recursive polymorphic types. Information and Control, 71(1–2):95–130, October–November 1986.

[9] Dana S. Scott. Lambda calculus: Some models, some philosophy. In Jon Barwise, H. Jerome Keisler, and Kenneth Kunen, editors, The Kleene Symposium, volume 101 of Studies in Logic and the Foundations of Mathematics, pages 223–265, Amsterdam, 1980. North-Holland.

[10] Andrej Bauer, Lars Birkedal, and Dana S. Scott. Equilogical spaces. To appear in Theoretical Computer Science, 2000.

[11] Anne Sjerp Troelstra, editor. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, 1973.

[12] Anne Sjerp Troelstra. Realizability. In Samuel R. Buss, editor, Handbook of Proof Theory, volume 137 of Studies in Logic and the Foundations of Mathematics, pages 407–473. Elsevier, Amsterdam, 1998.

[13] Georg Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In Arend Heyting, editor, Constructivity in Mathematics, pages 101–128. North-Holland, Amsterdam, 1959.

[14] S. C. Kleene. Countable functionals. In Arend Heyting, editor, Constructivity in Mathematics, pages 81–100. North-Holland, Amsterdam, 1959.

[15] Roberto M. Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi, volume 46 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, England, 1998.

[16] John C. Reynolds. The meaning of types — from intrinsic to extrinsic semantics. Research Series RS–00–32, BRICS, DAIMI, Department of Computer Science, University of Aarhus, December 2000.

[17] John C. Reynolds. An intrinsic semantics of intersection types (abstract of invited lecture). In Proceedings of the Workshop on Intersection Types and Related Systems, 2000. The slides for this lecture are available at ftp://ftp.cs.cmu.edu/user/jcr/intertype.ps.gz.