BRICS RS-02-34 M. Rhiger: A Foundation for Embedded Languages BRICS

Basic Research in Computer Science

A Foundation for Embedded Languages

Morten Rhiger BRICS Report Series RS-02-34 ISSN 0909-0878 August 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Morten Rhiger.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/02/34/

A Foundation for Embedded Languages

Morten Rhiger

BRICS ^{∗} Department of Computer Science University of Aarhus ^{†}

August, 2002

Abstract

Recent work on embedding object languages into Haskell use “phantom types” (i.e., parameterized types whose parameter does not occur on the right-hand side of the type definition) to ensure that the embedded object-language terms are simply typed. But is it a safe assumption that only simply-typed terms can be represented in Haskell using phantom types? And conversely, can all simply-typed terms be represented in Haskell under the restrictions imposed by phantom types? In this article we investigate the conditions under which these assumptions are true: We show that these questions can be answered affirmatively for an idealized Haskell-like language and discuss to which extent Haskell can be used as a meta-language.

∗ Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

† Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark.

E-mail: mrhiger@brics.dk Home page: http://www.brics.dk/~mrhiger New affiliation as of August 1, 2002:

The IT University in Copenhagen, Glentevej 67, DK-2400 Copenhagen NV, Denmark.

E-mail: mir@it-c.dk Home page: http://www.it-c.dk/~mir

Contents

1 Introduction 3

2 An embedded higher-order language 4 2.1 Higher-order abstract syntax . . . . . . . . . . . . . . . . . . . . 5 2.2 An embedded type discipline . . . . . . . . . . . . . . . . . . . . 5

3 Soundness and completeness 7 3.1 Object language . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.2 Meta-language . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

3.2.1 Denotational semantics . . . . . . . . . . . . . . . . . . . 9 3.3 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.4 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

4 Haskell as a meta-language 19 4.1 Extended object language . . . . . . . . . . . . . . . . . . . . . . 21 4.2 Extended meta-language . . . . . . . . . . . . . . . . . . . . . . . 23

5 Related work 23

6 Conclusions 25

List of Figures

1 Higher-order abstract syntax. . . . . . . . . . . . . . . . . . . . . 6 2 A typed higher-order language embedded into Haskell. . . . . . . 7 3 Extended object language. . . . . . . . . . . . . . . . . . . . . . . 21

1 Introduction

A program is typically written in terms of library routines. Once stabilized, it may itself become a library routine and be used in other programs. This bottomup style of programming makes program development and maintenance easier and more efficient since the programmer can rely on well-understood routines. One of the goals of module systems, macro systems, and separate compilation is precisely to ease the definition of new routines and the use of existing routines in new programs.

Similarly, new programming languages typically arise from extending (or, as Steele says [41], “growing”) existing languages with new features. Programming languages built from existing pieces are easier to design, implement, and understand since, in principle, they comprise well-understood components. For example, many realistic programming languages embody the λ-calculus as a core component. Yet, it was not until Scott that the λ-calculus itself was given a meaning. He warned that the hitherto “formalistic play with symbols” was useless and that, eventually, symbols must be given an interpretation [40]. Scott developed domain theory to provide a foundation for the λ-calculus. The result is the denotational semantics as we know it today in which the λ-calculus is used as a meta-language to define the semantics of programming languages [42].

A programming language can also be embedded into another, instead of directly giving its semantics in terms of, e.g., domains. The result combines the domain-specific operations (such as domain-specific values, their types, and operations on them) of the object language with the domain-independent linguistic features (such as evaluation strategy and type system) of the meta-language. (There is an unfortunate clash of terminology between formal domains as complete, partially ordered sets and informal domains as specific areas of applications.) Already in the 1960’s, this style was envisioned by Landin [26] who observed that the design of programming languages splits into “the choice of written appearances of programs” and “the choice of abstract entities that can be referred to in the language.”

Statically typed higher-order languages provide powerful domain-independ-ent linguistic features. In particular, the module system, type classes, and polymorphic types of Haskell [15] make it a natural candidate to host domainspecific components [23]. Examples of domain-specific languages embedded into Haskell include languages for geometric region analysis [3], interactive 3D animation [13], image synthesis and manipulation [14], interfacing with Microsoft’s Component Object Model [17, 25], music description and composition [24], accessing SQL databases [27], robot control [33], and real-time vision processing [37].

The domain-specific operations may be provided by an external system such as a graphical display showing images, a sound device playing music, a database processing SQL queries, or a robot executing orders; or they may be provided by an interpreter implemented in the meta-language. The domain-specific language may also provide a notion of well-typed domain-specific objects and restrict the range of the domain-specific operations to these objects. It is then crucial that only well-typed domain-specific objects can be expressed in the meta-language. When the object-language type system is sufficiently simple it can be expressed directly by the meta-language types of the domain-specific operations.

“Phantom types” were introduced to embed stronger object-language type systems into Haskell [17, 25, 27]. (We call a formal type parameter of a parameterized type “phantom” if all instances of the parameterized type are independent of the actual type parameters. A more informal characterization says that a phantom type is one that occurs on the left-hand side of a definition but not on the right, but this characterization does not catch situations where the righthand side does contain the type parameter but the type parameter is unused.) For example, phantom types are instrumental for embedding COM objects and for embedding SQL queries into Haskell [17, 25, 27]. They also provide a key for using Haskell’s type inferencer as a theorem prover to show that normalization functions as embodied in type-directed partial evaluation preserve types and yield normal forms [6, 7]. These applications of phantom types show that embedded type systems provide a powerful tool for both designing embedded programming languages and reasoning about program correctness. All existing embeddings using phantom types, however, take the following key properties for granted.

Type soundness: If a domain-specific object is ill-typed then it cannot be represented by a well-typed meta-language term.

Completeness: If a domain-specific object is well-typed then it can be represented by a well-typed meta-language term.

Together, these properties simply states that the meta-language type system accepts exactly the well-typed object-language terms. In other words, the objectlanguage type system is correctly simulated by the meta-language. In this work we formally prove that these properties hold when embedding a monomorphic, higher-order language into an idealized Haskell-like meta-language.

This paper is organized as follows. Section 2 gives an implementation of an embedding of the terms and types of the simply typed λ-calculus into Haskell. In Section 3 we present a semantics of an idealized Haskell-like meta-language and then prove the two properties mentioned above. In Section 4 we investigate the use of Haskell as a meta-language, in particular, which precautions to take when Haskell is used as a meta-language. This section also discusses extensions to the object and meta-languages. Section 5 gives an overview of related work and Section 6 concludes.

2 An embedded higher-order language

Let us consider a domain-specific object language for manipulating integers and higher-order functions, i.e., an extension of the simply typed λ-calculus. We include addition of integers but, depending on the domain, one can add other base types, finite products, lists, etc. and primitive operations on these types. In Haskell, the object language can be represented by the following data type.

   type Ide = String
   data Raw = INT Int | ADD Raw Raw
            | VAR Ide | LAM Ide Raw | APP Raw Raw
   instance Show Raw where
     showsPrec _t = ...

Here we have equipped the data type with a function showing terms as strings. An alternative to using a data type is to directly encode terms as strings (if, for example, terms are passed to an external system as concrete syntax).

2.1 Higher-order abstract syntax

The key to embedding a typed higher-order object language is to use higherorder abstract syntax [35] as the interface to constructing terms. In higher-order abstract syntax, variables and bindings of the object language are modelled by variables and bindings of the meta-language, in this case Haskell. It is precisely this connection that enables meta-language types to model objectlanguage types.

A higher-order abstract syntax usually carries higher-order functions in the representation of lambdas. The following data type illustrates such a minimal higher-order abstract syntax.

   data HoExp = LAM (HoExp    HoExp) | APP HoExp HoExp

However, short of higher-order matching in Haskell, elements of this data type cannot be decomposed. Therefore, we build (and reason about) first-order syntax. In order to maintain the connection between bindings in the object language and the meta-language we construct first-order syntax using a higherorder interface as illustrated in Figure 1. The higher-order implementation hides the (first-order) constructors for variables and lambdas; instead a new higherorder constructor groups together the construction of a symbolic variable and the lambda that binds it.

To facilitate automatic generation of variable names, terms are abstracted over a list of fresh variable names. (Generally, these names must be distinct to prevent variable clashes in the raw representation of the term.) The type of terms are [Ide] Raw. The same list of variable names is passed to all subterms, except in the case of lambdas where the first name is used to construct a symbolic variable and the rest of the names are passed to the body of the lambda. Each variable in a term is therefore assigned the ith name in the given list where i is the de Bruijn level [9] of the variable in the term. For example, using the names ["a", "b"] to construct the first-order term of

lam ( x   app (lam ( y   y)) (lam ( z   z))) yields
        LAM "a" (APP (LAM "b" (VAR "b")) (LAM "b" (VAR "b")))

2.2 An embedded type discipline

Unfortunately, the higher-order abstract syntax does not impose any type constraints on the embedded language. For example, Haskell accepts the expression

   module Lambda(Exp, int, add, lam, app) where
     ...
     type Exp = [Ide]    Raw
     int :: Int    Exp
     add :: Exp    Exp    Exp
     lam :: (Exp    Exp)    Exp
     app :: Exp    Exp    Exp
     int i   =  ns    INT i
     add a b =  ns    ADD (a ns) (b ns)
     lam f   =  (n:ns)    LAM n (f ( z  VAR n) ns)
     app a b =  ns    APP (a ns) (b ns)

Figure 1: Higher-order abstract syntax.

                     app (int 1) (lam ( x   x))

even though its value represents the ill-typed object-language term (here presented in Haskell syntax) 1 ( x x).

Therefore, we restrict the higher-order constructors to only yield representations of well-typed terms. To this end, we make the following observations about constructing representations of well-typed object-language terms:

• int produces an object-language term of type Int.

• When add is applied to two object-language terms of type Int it produces an object-language term of type Int.

• When app is applied to two object-language terms of types a b and a it produces a term of object-language type b.

• When lam is applied to a function mapping an object-language term of type a into an object-language term of type b it produces an objectlanguage term of type a b.

These dependencies are just verbal formulations of the standard type rules for the simply-typed λ-calculus. They suggest that the (polymorphic) types of the constructors actually could reflect the object-language types. We thus parameterize the type Exp over the type of the represented object-language term and we restrict the types of the constructors according to the observations above. The type parameter of Exp is a phantom type: it is not used in the right-hand side of the definition of Exp.

The complete embedding of the simply-typed λ-calculus into Haskell is shown in Figure 2. Terms are given by an abstract data type: a newtype declaration hides their representations as functions of type [Ide] Raw and the module only exports the typed constructors.

   module Lambda(Exp, int, add, lam, app) where
     type Ide = String
     data Raw = INT Int | ADD Raw Raw
              | VAR Ide | LAM Ide Raw | APP Raw Raw
     newtype Exp t = E ([Ide]    Raw)
     make (E a) ns = a ns
     int :: Int    Exp Int
     add :: Exp Int    Exp Int    Exp Int
     lam :: (Exp a    Exp b)    Exp (a    b)
     app :: Exp (a    b)    Exp a    Exp b
     int i   = E ( ns    INT i)
     add a b = E ( ns    ADD (make a ns) (make b ns))
     lam f   = E ( (n:ns)    LAM n (make (f (E ( z  VAR n))) ns))
     app a b = E ( ns    APP (make a ns) (make b ns))
     instance Show (Exp t) where
       showsPrec i (E a) = showsPrec i r where
         r = a [c:i | i  ("":map show [1..]), c  ['a'..'z']]

Figure 2: A typed higher-order language embedded into Haskell.

As an example, Haskell rejects the expression app (int 1) (lam ( x x)), since this expression is an attempt to represent the ill-typed object-language term 1 ( x x). On the other hand, the object-language term f 2 + (f 1) has the type (Int Int) Int. It can thus be represented in Haskell by

lam ( f   add (int 2) (app f (int 1))) of type Exp ((Int   Int)   Int).

It is, however, not clear just from the implementation in Figure 2 and the inferred types that all ill-typed terms are ruled out. Nor is it clear that all well-typed term are not ruled out. In the next section we present an idealized Haskell-like meta-language in which these properties do hold.

3 Soundness and completeness

We introduce the the syntax and type system of a simply typed λ-calculus (the object language) with constants of base type. We then consider an idealized meta-language without let-polymorphism but with a set of predefined polymorphic constant symbols. We give the syntax, type system, and denotational semantics of the meta-language. Soundness follows from a proof using a Kripke logical relation and completeness follows by structural induction. Section 4 discusses the differences between the idealized meta-language and Haskell.

3.1 Object language

To reason about object-language types and terms we use the following concrete representations.

\begin{aligned}σ & ::= & Int | σ_{1} → σ_{2} \\ u & ::= & i | u_{1} + u_{2} | x | λx.u | u_{1} u_{2} \end{aligned}

We let Δ range over finite mappings from variables to object-language types. The following type rules assigns types to object-language terms.

\overline{Δ ⊢ i : Int}  \frac{Δ ⊢ u_{1} : Int Δ ⊢ u_{2} : Int}{Δ ⊢ u_{1} + u_{2} : Int}

\frac{Δ(x) = σ}{Δ ⊢ x : σ}  \frac{Δ[x : σ_{1}] ⊢ u : σ_{2}}{Δ ⊢ λx.u : σ_{1} → σ_{2}}  \frac{Δ ⊢ u_{1} : σ_{1} → σ_{2} Δ ⊢ u_{2} : σ_{1}}{Δ ⊢ u_{1} u_{2} : σ_{2}}

These rules are standard and standard results apply to them. We shall only need the following weakening lemma.

Lemma 1 (Weakening). If for all x ∈ dom(Δ), Δ′(x) = Δ(x) and Δ ⊢ u : σ then Δ′ ⊢ u : σ

Proof. By induction on the derivation of Δ ⊢ u : σ.

3.2 Meta-language

Let β range over a set B of base types. The types of the meta-language consist of base types, function types, and types of representations of terms.

τ ::= β | τ_{1} → τ_{2} | Exp σ

In the type Exp σ, the intention is that σ is the type of the represented objectlanguage term (as also suggested by the examples at the end of Section 2). By construction, this σ cannot itself contain occurrences of Exp . This means that the object language cannot itself express encoded terms, such as used in a multi-stage framework.

Let x range over an infinite set V of variable names and c_{t_{1}···t_{n}} over a set C of constant symbols. The type of a constant c_{t_{1}···t_{n}} may depend on t_{1}, …, t_{n}, where each t_{i} is either a meta-language type τ or an object-language type σ. (The type of the constant will always be a meta-language type.) Hence, a constant symbol c_{t_{1}···t_{n}} corresponds to a particular monomorphic instance of a polymorphic constant symbol c. For example, a polymorphic identity function could be introduced by the set of constants {id_{τ} | type τ} where each id_{τ} would be given type τ → τ. (The assignment of types to constant symbols is discussed below.) The syntax of our small language is now given as follows.

e ::= x | λx.e | e_{1} e_{2} | c_{t_{1}···t_{n}} | rec x.e

A signature Σ = (B, C) lists base types and constant symbols and additionally assigns types Σ(c_{t_{1}···t_{n}}) to constants c_{t_{1}···t_{n}}. A type context Γ is a finite mapping from variables to types. Given a signature Σ, the type rules for the language are as follows.

\frac{Γ(x) = τ}{Γ ⊢_{Σ} x : τ} \frac{Γ[x : τ_{1}] ⊢_{Σ} e : τ_{2}}{Γ ⊢_{Σ} λx.e : τ_{1} → τ_{2}} \frac{Γ ⊢_{Σ} e_{1} : τ_{2} → τ Γ ⊢_{Σ} e_{2} : τ_{2}}{Γ ⊢_{Σ} e_{1} e_{2} : τ}

\frac{Σ(c_{t_{1}···t_{n}}) = τ}{Γ ⊢_{Σ} c_{t_{1}···t_{n}} : τ} \frac{Γ[x : τ] ⊢_{Σ} e : τ}{Γ ⊢_{Σ} rec x.e : τ}

We define a base signature Σ_{0} = (B_{0}, C_{0}) containing an addition function and higher-order constructors,

B_{0} = {Int}
C_{0} = Z ∪ {+, int, add} ∪ ⋃_{types σ_{1},σ_{2}}{lam_{σ_{1},σ_{2}}, app_{σ_{1},σ_{2}}}

where Z is the set of integers. The associated assignment of types to constant symbols is given as follows. (This is where the types of the higher-order constructors are restricted.)

Σ_{0}(i) = Int, for each i ∈ Z Σ_{0}(int) = Int → Exp Int
Σ_{0}(+) = Int → Int → Int  Σ_{0}(add) = Exp Int → Exp Int → Exp Int
Σ_{0}(lam_{σ_{1},σ_{2}}) = (Exp σ_{1} → Exp σ_{2}) → Exp (σ_{1} → σ_{2})
Σ_{0}(app_{σ_{1},σ_{2}}) = Exp (σ_{1} → σ_{2}) → Exp σ_{1} → Exp σ_{2}

It is straightforward to extend the meta-language with other base types and constant symbols. The formal requirements that constant symbols must satisfy are discussed in Section 3.3.

3.2.1 Denotational semantics

To model the construction of object-language terms, we assume the existence of a discretely ordered [45, page 120] set L that is capable of representing terms and we assume the existence of the following injective functions with mutually disjoint ranges,

INT ∈ Z → L  ADD ∈ L × L → L
VAR ∈ V → L  LAM ∈ V × L → L
APP ∈ L × L → L

where N is the set of natural numbers. As an example one might take L to be, e.g., the set of finite strings of symbols. We need not require the constructor functions to be surjective. That is, we do not rule out “syntactically invalid” elements in L.

We draw fresh object-language variables from the same source as metalanguage variables, namely the infinite set V. In particular, we assume that there is an injective function fresh ∈ N → V.

In the semantical development that follows we shall use standard domaintheoretic notation: For CPOs A and B, we write A_{⊥} for the lifted domain, ⊥_{A} for the bottom element of this domain, up ∈ A → A_{⊥} for the lifting injection, f^{∗} ∈ A_{⊥} → B_{⊥} for the strict extension of f ∈ A → B_{⊥}, f_{⊥} ∈ A_{⊥} → B_{⊥} for the strict version of f ∈ A → B. We shall write (·, ·)_{⊥} ∈ A_{⊥}×B_{⊥} → (A × B)_{⊥} for the strict pairing function, e.g., the function for which (up(a), up(b))_{⊥} = up(a, b) and where (a, b)_{⊥} = ⊥_{A×B} if either a = ⊥_{A} or b = ⊥_{B}. We write A →_{c} B for the continuous function space between A and B. The partial order on a domain A is ⊏_{A}.

An interpretation I of a signature Σ assigns predomains (i.e., bottomless CPOs) to base types and values to constant symbols. For a given interpretation I, the meaning of types is defined as follows. (In the third case, σ is the semantic counterpart of a phantom type: it does not affect the predomain assigned to Exp σ.)

\begin{aligned}[[β]]_{I} & = & (I(β))_{⊥} \\ [[τ_{1} → τ_{2}]]_{I} & = & [[τ_{1}]]_{I} →_{c} [[τ_{2}]]_{I} \\ [[Exp σ]]_{I} & = & N_{⊥} →_{c} L_{⊥} \end{aligned}

The interpretation furthermore assigns values to constant symbols such that if Σ(c_{t_{1}···t_{n}}) = τ then I(c_{t_{1}···t_{n}}) ∈ [[τ]]_{I}.

The meaning of a type context Γ is the labelled product

[[Γ]]_{I} = ∏_{x∈dom(Γ)}[[Γ(x)]]_{I}

Finally, to any well-typed meta-language expression Γ ⊢_{Σ} e : τ we assign a continuous function [[e]]_{I} ∈ [[Γ]]_{I} →_{c} [[τ]]_{I}. The following is a standard call-by-name semantics for functional languages.

[[x]]_{I} ρ = ρ(x)
[[λx.e]]_{I} ρ = λa.[[e]]_{I} ρ[x ↦ a]
[[e_{1} e_{2}]]_{I} ρ = [[e_{1}]]_{I} ρ ([[e_{2}]]_{I} ρ)
[[c_{t_{1}···t_{n}}]]_{I} ρ = I(c_{t_{1}···t_{n}})
[[rec x.e]]_{I} ρ = ⨆_{i∈ω} ϕ^{i}(⊥_{[[τ]]_{I}}), where ϕ(a) = [[e]]_{I} ρ[x ↦ a]

The initial signature Σ_{0} is given the interpretation I_{0}: First, the type Int is interpreted by the integers, i.e., I_{0}(Int) = Z. For the constant symbols, the interpretation is defined as follows.

I_{0}(i) = up(i)
I_{0}(+) = λx.λy.x +_{⊥} y
I_{0}(int) = λi.λn.INT_{⊥}(i)
I_{0}(add) = λv_{1}.λv_{2}.λn.ADD_{⊥}(v_{1}(n), v_{2}(n))_{⊥}
I_{0}(lam_{σ_{1},σ_{2}}) = λf.λn.LAM_{⊥}(fresh_{⊥}(n),

f (λz.VAR_{⊥}(fresh_{⊥}(n))) (n +_{⊥} up(1)))_{⊥}

I_{0}(app_{σ_{1},σ_{2}}) = λv_{1}.λv_{2}.λn.APP_{⊥}(v_{1}(n), v_{2}(n))_{⊥}

The two last equations hold for all object-language types σ_{1} and σ_{2}.

It follows by construction that the functions involved in defining the semantics of terms and in defining the initial interpretation of the constant symbols are all continuous.

We define the obvious injective representation functions mapping objectlanguage terms into L as follows.

⌈i⌉ = INT (i)  ⌈u_{1} + u_{2}⌉ = ADD(⌈u_{1}⌉, ⌈u_{2}⌉)
⌈x⌉ = VAR(x)  ⌈λx.u⌉ = LAM (x, ⌈u⌉)
⌈u_{1} u_{2}⌉ = APP(⌈u_{1}⌉, ⌈u_{2}⌉)

This representation function need not be surjective: Some elements in L may not correspond to any object-language term. It is our goal to show, however, that any element of L that is denoted by an expression in the meta-language corresponds to an object-language term and, furthermore, that these terms are well typed.

3.3 Soundness

In this section we formally state and prove soundness. We end up with Corollary 1, a strong soundness result stating that if an expression has type Exp σ then it either diverges or yields the representation of an object-language term of type σ, and Corollary 2, a weak result that corresponds to the informal statement from Section 1.

In the rest of this section we restrict our attention to the initial signature Σ_{0} and the initial interpretation I_{0}.

Definition 1. Given a type context Δ and a type σ we define a subset of L_{⊥} as follows.

T_{σ}^{Δ} = {⊥_{L}} ∪ {up(l) ∈ L_{⊥} | ∃u.⌈u⌉ = l ∧ Δ ⊢ u : σ}

The set T_{σ}^{Δ} contains exactly the elements in L_{⊥} that are undefined or that correspond to object-language terms of type σ in type context Δ.

Lemma 2 (Admissibility of T ). For any type σ and type context Δ the relation T_{σ}^{Δ} is admissible. That is, it is pointed (i.e., ⊥_{L} ∈ T_{σ}^{Δ}) and it is chain complete (i.e., if (l_{i})_{i∈ω} is a chain in L_{⊥} such that for all i ∈ ω, l_{i} ∈ T_{σ}^{Δ} then ⨆_{i∈ω} l_{i} ∈ T_{σ}^{Δ}).

Proof. Pointedness follows trivially by the definition. Chain completeness follows from the fact that L_{⊥} is discretely ordered and that any chain in L_{⊥} therefore eventually becomes constant.

Definition 2. A world is a type context Δ. Worlds are ordered as follows.

Δ′ ⪰ Δ ⟺ ∀x ∈ dom(Δ).x ∈ dom(Δ′) ∧ Δ′(x) = Δ(x)

We let #Δ = max({−1} ∪ {i | fresh(i) ∈ dom(Δ)}) denote the largest fresh variable number already bound in the context Δ (or −1 if the context is empty).

It is easy to show that ⪰ is reflexive and transitive, that Δ′ ⪰ Δ implies #Δ′ ≥ #Δ, and that n > #Δ implies n + 1 > #Δ[g : σ] where g = fresh(n).

Terms that are well typed in one world are also well typed in any larger world, a result due to weakening.

Lemma 3 (Monotonicity of T ). For any type σ, if two type contexts satisfy Δ′ ⪰ Δ then T_{σ}^{Δ′} ⊇ T_{σ}^{Δ}.

Proof. A consequence of Lemma 1.

A logical relation is a type-indexed relation over the denoted values defined in such a way that it is closed under abstraction and application [30]. We define such a unary logical relation containing values that behave well: Informally, all values of base type are well-behaved, a function is well-behaved if it maps well-behaved values to well-behaved result, and a representation of an objectlanguage term is well-behaved if, given a fresh variable index, it has the correct type in a given type context.

Definition 3 (Logical relation R). Given a type τ and a type context Δ we define a subset of [[τ]]_{I_{0}} as follows.

(1) R_{β}^{Δ} = [[β]]_{I_{0}}

(2) R_{τ_{1}→τ_{2}}^{Δ} = {f ∈ [[τ_{1}]]_{I_{0}} →_{c} [[τ_{2}]]_{I_{0}} | ∀Δ′ ⪰ Δ.∀a ∈ R_{τ_{1}}^{Δ′}.f(a) ∈ R_{τ_{2}}^{Δ′}}

(3) R_{Exp σ}^{Δ} = {f ∈ N_{⊥} →_{c} L_{⊥} | ∀n > #Δ.f(up(n)) ∈ T_{σ}^{Δ}}

In case (2), the restriction that f ∈ R_{τ_{1}→τ_{2}}^{Δ} must satisfy f(R_{τ_{1}}^{Δ′}) ⊆ R_{τ_{2}}^{Δ′} for any Δ′ ⪰ Δ (and not just for Δ′ = Δ) accounts for situations where an argument to such a function carries free object-language variables not contained in Δ. This is utilized in showing soundness for lam_{σ_{1},σ_{2}} (which introduces free object-language variables) in Lemma 8 below. The restriction also ensures that the logical relation is monotone.

The goal is now to show that any well-typed meta-language expression denotes a well-behaved value.

Lemma 4 (Admissibility of R_{τ}). For any type τ and type context Δ the relation R_{τ}^{Δ} is admissible.

Proof. Using admissibility of T_{σ}^{Δ} (Lemma 2). Chain completeness follows by induction on τ. For the case τ = β we use the fact R_{β}^{Δ} is the constantly true predicate. For the case τ = Exp σ we use chain completeness of T_{σ}^{Δ} and the fact that for any chain of continuous functions (f_{n})_{n∈ω}, (⨆_{n∈ω} f_{n}) (x) = ⨆_{n∈ω} f_{n}(x). Pointedness follows by induction on τ using pointedness of T_{σ}^{Δ} and [[β]]_{I_{0}}.

Together with Definition 3, the following lemma shows that R_{τ} is a Kripke logical relation [30].

Lemma 5 (Monotonicity of R_{τ}). For any type τ, if two type contexts satisfy Δ′ ⪰ Δ then R_{τ}^{Δ′} ⊇ R_{τ}^{Δ}.

Proof. By induction on τ.

Case τ = β. Holds trivially since R_{β}^{Δ′} = R_{β}^{Δ}.

Case τ = τ_{1} → τ_{2}. Follows from the transitivity of ⪰.

Case τ = Exp σ. Follows from the monotonicity of T (Lemma 3) and using the fact that #Δ′ ≥ #Δ.

We extend the logical relation of values and types to a relation of environments and type contexts. This gives a notion of well-behaved environments.

Definition 4. For any type contexts Δ and Γ we define a subset of [[Γ]]_{I_{0}} as follows.

R_{Γ}^{Δ} = {ρ ∈ [[Γ]]_{I_{0}} | ∀x ∈ dom(Γ).ρ(x) ∈ R_{Γ(x)}^{Δ}}

This extension preserves monotonicity.

Lemma 6 (Monotonicity of R_{Γ}). For all type contexts Γ, Δ, and Δ′, if Δ′ ⪰ Δ then R_{Γ}^{Δ′} ⊇ R_{Γ}^{Δ}.

Proof. Follows from Lemma 5.

Adding a well-behaved value to an already well-behaved environment results in another well-behaved environment.

Lemma 7. If d ∈ R_{τ}^{Δ} and ρ ∈ R_{Γ}^{Δ} then also ρ[x ↦ d] ∈ R_{Γ[x:τ]}^{Δ}.

Proof. Follows from Definition 4.

Using the results established so far, soundness amounts to showing that the semantics of a well-typed expression is well-behaved. The following lemma shows that this result holds for the constant symbols defined by the initial interpretation.

Lemma 8. For any constant symbol c_{t_{1}···t_{n}} ∈ C_{0} with Σ_{0}(c_{t_{1}···t_{n}}) = τ and for any type context Δ we have I_{0}(c_{t_{1}···t_{n}}) ∈ R_{τ}^{Δ}.

Proof. By analysis of the individual constant symbols.

Case c_{t_{1}···t_{n}} = i. Holds trivially since all values of base type are well behaved.

Case c_{t_{1}···t_{n}} = +. Holds trivially since + produces a value of base type which is always well behaved.

Case c_{t_{1}···t_{n}} = int. Since Δ ⊢ i : Int we have up(INT (i)) ∈ T_{Int}^{Δ} for any i ∈ Z and type context Δ. Therefore λi.λn.INT_{⊥}(up(i)) = λi.λn.up(INT (i)) ∈

R_{Int→Exp Int}^{Δ} as required.

Case c_{t_{1}···t_{n}} = add. Given Δ′ ⪰ Δ, Δ′′ ⪰ Δ′, v_{1} ∈ R_{Exp Int}^{Δ′}, v_{2} ∈ R_{Exp Int}^{Δ′′}, and n > #Δ′′ we must show that ADD_{⊥}(v_{1}(up(n)), v_{2}(up(n)))_{⊥} is either ⊥_{L} or equal to up ⌈u⌉ for some u with Δ′′ ⊢ u : Int. Since n > #Δ′′ ≥ #Δ′ ≥ #Δ we immediately have v_{2}(up(n)) ∈ T_{Int}^{Δ′′}. Using Lemma 3 we also get v_{1}(up(n)) ∈ T_{Int}^{Δ′} ⊆ T_{Int}^{Δ′′}. Therefore, either v_{1}(up(n)) = ⊥_{L} or v_{2}(up(n)) = ⊥_{L}, in which case we are done since ADD_{⊥}(v_{1}(up(n)), v_{2}(up(n)))_{⊥} = ⊥_{L}, or we have terms u_{1} and u_{2} with v_{1}(up(n)) = up ⌈u_{1}⌉, v_{2}(up(n)) = up ⌈u_{2}⌉, Δ′′ ⊢ u_{1} : Int, and Δ′′ ⊢ u_{2} : Int. We set u = u_{1} + u_{2} and have

ADD_{⊥}(v_{1}(up(n)), v_{2}(up(n)))_{⊥} = up ⌈u_{1} + u_{2}⌉

and

\frac{Δ′′ ⊢ u_{1} : Int Δ′′ ⊢ u_{2} : Int}{Δ′′ ⊢ u_{1} + u_{2} : Int}

as required.

Case c_{t_{1}···t_{n}} = lam_{σ_{1},σ_{2}}. Given Δ′ ⪰ Δ, n > #Δ′, g = fresh(n), and f ∈ R_{Exp σ_{1}→Exp σ_{2}}^{Δ′} we must show that

LAM_{⊥}(up(g), f (λz.VAR_{⊥}(up(g))) (up(n + 1)))_{⊥}

is either ⊥_{L} or equal to up ⌈u⌉ for some u with Δ′ ⊢ u : σ_{1} → σ_{2}

We have λz.VAR_{⊥}(up(g)) = λz.up(VAR(g)) ∈ R_{Exp σ_{1}}^{Δ′[g:σ_{1}]} since ⌈g⌉ = VAR(g) and Δ′[g : σ_{1}] ⊢ g : σ_{1}. Since also n + 1 > #(Δ′[g : σ_{1}]) we have

f (λz.VAR_{⊥}(up(g))) (up(n + 1)) ∈ T_{σ_{2}}^{Δ′[g:σ_{1}]}

This value must therefore either be ⊥_{L}, in which case we are done, or be equal to up ⌈u′⌉ for some term u′ with Δ′[g : σ_{1}] ⊢ u′ : σ_{2}. We set u = λg.u′ and have

LAM_{⊥}(up(g), f (λz.VAR_{⊥}(up(g))) (up(n + 1)))_{⊥} = up ⌈λg.u′⌉

and

\frac{Δ′[g : σ_{1}] ⊢ u′ : σ_{2}}{Δ′ ⊢ λg.u′ : σ_{1} → σ_{2}}

as required.

Case c_{t_{1}···t_{n}} = app_{σ_{1},σ_{2}}. (Follows the same structure as the case for add.) Given Δ′ ⪰ Δ, Δ′′ ⪰ Δ′, v_{1} ∈ R_{Exp (σ_{1}→σ_{2})}^{Δ′}, v_{2} ∈ R_{Exp σ_{1}}^{Δ′′}, and n > #Δ′′ we must show that APP_{⊥}(v_{1}(up(n)), v_{2}(up(n)))_{⊥} is either ⊥_{L} or equal to up ⌈u⌉ for some u with Δ′′ ⊢ u : σ_{2}. Since n > #Δ′′ ≥ #Δ′ ≥ #Δ we immediately have v_{2}(up(n)) ∈ T_{σ_{1}}^{Δ′′}. Using Lemma 3 we also get v_{1}(up(n)) ∈ T_{σ_{1}→σ_{2}}^{Δ′} ⊆ T_{σ_{1}→σ_{2}}^{Δ′′}. Therefore, either v_{1}(up(n)) = ⊥_{L} or v_{2}(up(n)) = ⊥_{L}, in which case we are done since APP_{⊥}(v_{1}(up(n)), v_{2}(up(n)))_{⊥} = ⊥_{L}, or we have terms u_{1} and u_{2} with v_{1}(up(n)) = up ⌈u_{1}⌉, v_{2}(up(n)) = up ⌈u_{2}⌉, Δ′′ ⊢ u_{1} : σ_{1} → σ_{2}, and Δ′′ ⊢ u_{2} : σ_{1}. We set u = u_{1} u_{2} and have

APP_{⊥}(v_{1}(up(n)), v_{2}(up(n)))_{⊥} = up ⌈u_{1} u_{2}⌉

and

\frac{Δ′′ ⊢ u_{1} : σ_{1} → σ_{2} Δ′′ ⊢ u_{2} : σ_{1}}{Δ′′ ⊢ u_{1} u_{2} : σ_{2}}

as required.

Other constant symbols can be added to the meta-language if they satisfy Lemma 8. The following main result states that evaluating a well-typed expression in a well-behaved environment yields a well-behaved value.

Theorem 1 (Soundness). In the initial interpretation I_{0} of the initial signature Σ_{0}, if Γ ⊢_{Σ_{0}} e : τ and ρ ∈ R_{Γ}^{Δ} then [[e]]_{I_{0}} ρ ∈ R_{τ}^{Δ}.

Proof. By structural induction on e.

Case e = x. Then Γ(x) = τ and [[x]]_{I_{0}} ρ = ρ(x) so [[x]]_{I_{0}} ρ ∈ R_{τ}^{Δ} follows from Definition 4.

Case e = λx.e′. Then τ = τ_{1} → τ_{2} where Γ[x : τ_{1}] ⊢_{Σ_{0}} e′ : τ_{2} and [[λx.e′]]_{I_{0}} ρ = λa.[[e′]]_{I_{0}} ρ[x ↦ a]. We must show [[λx.e′]]_{I_{0}} ρ ∈ R_{τ_{1}→τ_{2}}^{Δ}. So given Δ′ ⪰ Δ and d ∈ R_{τ_{1}}^{Δ′} we must show that [[e′]]_{I_{0}} ρ[x ↦ d] ∈ R_{τ_{2}}^{Δ′}. From Lemma 6 it follows that ρ ∈ R_{Γ}^{Δ′} and then from Lemma 7 we have that ρ[x ↦ d] ∈ R_{Γ[x:τ_{1}]}^{Δ′}. Thus, [[e′]]_{I_{0}} ρ[x ↦ d] ∈ R_{τ_{2}}^{Δ′} follows from the induction hypothesis.

Case e = e_{1} e_{2}. Then Γ ⊢_{Σ_{0}} e_{1} : τ_{2} → τ, Γ ⊢_{Σ_{0}} e_{2} : τ_{2}, and [[e_{1} e_{2}]]_{I_{0}} ρ = [[e_{1}]]_{I_{0}} ρ ([[e_{2}]]_{I_{0}} ρ). Using the induction hypothesis twice we get [[e_{1}]]_{I_{0}} ρ ∈ R_{τ_{2}→τ}^{Δ} and [[e_{2}]]_{I_{0}} ρ ∈ R_{τ_{2}}^{Δ}. Using reflexivity of ⪰, Definition 3(2) gives [[e_{1} e_{2}]]_{I_{0}} ρ ∈ R_{τ}^{Δ} as required.

Case e = c_{t_{1}···t_{n}}. Follows from Lemma 8.

Case rec x.e′. Using pointedness for the base case and Lemma 7 for the induction step an induction on i shows that ϕ^{i}(⊥) ∈ R_{τ}^{Δ} for all i, where ϕ(a) = [[e′]]_{I_{0}} ρ[x ↦ a] . The result then follows from admissibility (Lemma 4).

The following corollary states that an expression of type Exp σ evaluates to a function that, when passed an initial variable index, either diverges or yields a representation of an object-language term of type σ.

Corollary 1. For any σ and e if ∅ ⊢_{Σ_{0}} e : Exp σ then either

(1) [[e]]_{I_{0}} ∅ (up(0)) = ⊥_{L}, or

(2) [[e]]_{I_{0}} ∅ (up(0)) = up ⌈u⌉ for some term u with ∅ ⊢ u : σ.

Proof. Since ∅ ∈ R_{∅}^{∅}, Theorem 1 gives

[[e]]_{I_{0}} ∅ ∈ R_{Exp σ}^{∅} = {f ∈ N_{⊥} →_{c} L_{⊥} | ∀n > #∅.f(up(n)) ∈ T_{σ}^{∅}}

In particular, since #∅ = −1

[[e]]_{I_{0}} ∅ (up(0)) ∈ T_{σ}^{∅} = {⊥_{L}} ∪ {up(l) ∈ L_{⊥} | ∃u.⌈u⌉ = l ∧ ∅ ⊢ u : σ}

From which the result follows.

The above corollary is a strong soundness result that relates types of metalanguage expressions to types of object-language terms. In analogy with the informal statement in Section 1 we also have the following weaker result about the mere existence of object-language terms.

Corollary 2. Given an object-language term u, if, for any σ, ∅ ⊬ u : σ then there exist no e and σ with ∅ ⊢_{Σ_{0}} e : Exp σ and [[e]]_{I_{0}} ∅ (up(0)) = up ⌈u⌉.

Proof. Follows from Corollary 1 by a proof of contradiction.

3.4 Completeness

We show that for any well-typed object-language term there exists a metalanguage expression that evaluates to a representation of the term. It is straightforward to translate an object-language term into a Haskell expression that builds a representation of that term. Using the definitions in Figure 2, such a translation can be defined by induction over object-language terms as follows. (We rely on the requirement that the object-languages identifiers are a subset of the Haskell identifiers.)

⟨x⟩ = x  ⟨λx.u⟩ = lam ( x ⟨u⟩)
⟨i⟩ = int i  ⟨u_{1} u_{2}⟩ = app ⟨u_{1}⟩ ⟨u_{2}⟩
⟨u_{1} + u_{2}⟩ = add ⟨u_{1}⟩ ⟨u_{2}⟩

However, the idealized meta-language used in our formal development provides type-indexed constant symbols instead of polymorphic functions such as lam and app. We therefore present the translation as an extended type system where the constant symbols are indexed by the correct types. The translation uses int, add, lam_{σ_{1},σ_{2}}, and app_{σ_{1},σ_{2}} to build integers, additions, lambdas, and applications. In addition, the type rules carry symbolic variable indices so that these can be related to the corresponding meta-language variables in the proofs below.

We let a translation context Ξ range over finite mappings from variables to pairs of types and integers. It is the intention that these integers denote the de Bruijn levels of the free variables in the term. The following rules then simply add a translation to the type system presented in Section 3.1. They define a predicate n; Ξ ⊢ e : σ / e expressing that at de Bruijn level n and in translation context Ξ the object-language term u has type σ and it translates to the meta-language expression e.

\overline{n; Ξ ⊢ i : Int / int i} \frac{n; Ξ ⊢ u_{1} : Int / e_{1} n; Ξ ⊢ u_{2} : Int / e_{2}}{n; Ξ ⊢ u_{1} + u_{2} : Int / add e_{1} e_{2}}

\frac{Ξ(x) = (σ, m)}{n; Ξ ⊢ x : σ / x} \frac{n + 1; Ξ[x : (σ_{1}, n)] ⊢ u : σ_{2} / e}{n; Ξ ⊢ λx.u : σ_{1} → σ_{2} / lam_{σ_{1},σ_{2}} (λx.e)}

\frac{n; Ξ ⊢ u_{1} : σ_{1} → σ_{2} / e_{1} n; Ξ ⊢ u_{2} : σ_{1} / e_{2}}{n; Ξ ⊢ u_{1} u_{2} : σ_{2} / app_{σ_{1},σ_{2}} e_{1} e_{2}}

As shown by the following lemma, if an object-language term can be typed in the type system presented in Section 3.1 then it can also be translated in the system above. We say that a type context Δ and a translation context Ξ are related by Δ ≈ Ξ when dom(Δ) = dom(Ξ) and when for all x ∈ dom(Δ), Δ(x) = σ implies Ξ(x) = (σ, m) for some m.

Lemma 9. If Δ ⊢ u : σ, Δ ≈ Ξ, and n denotes the number of free variables in u then there exists an expression e such that n; Ξ ⊢ u : σ / e.

Proof. By induction on the derivation of Δ ⊢ u : σ.

We first relate the type of the object-language term and the type of the meta-language expression it is translated to.

Lemma 10. For any translation context Ξ, type context Γ, n ∈ Z, and type σ, if n; Ξ ⊢ u : σ / e and if Γ(x) = Exp σ when Ξ(x) = (σ, n) then Γ ⊢_{Σ_{0}} e : Exp σ

Proof. By induction on the derivation of n; Ξ ⊢ u : σ / e.

Not all well-typed object-language terms can be encoded syntactically in the meta-language since the fresh variable names drawn from the predetermined list might differ from the intended variable names. We will show, however, that a term and its encoding as given above are equal up to renaming of bound variables.

Definition 5 (Substitutions and α-convertibility). A substitution s is a finite mapping of variables to variables. We let (s\x) be the restricted substitution satisfying (s\x) (x) = x and (s\x) (y) = s(y) for x ≠ y. Substitutions extend to terms in such a way that s(λx.u) = λx.u′ where u′ = (s\x) (u).

We say that a term u can be α-converted to a term u′ under a substitution s, written s ⊢ u ⟶ u′, if renaming bound variables in u according to s yields u′. The relation is defined by the following rules.

\overline{s ⊢ i ⟶ i} \frac{s(x) = y}{s ⊢ x ⟶ y} \frac{y ∉ (s\x) (u) s[x ↦ y] ⊢ u ⟶ u′}{s ⊢ λx.u ⟶ λy.u′}

\frac{s ⊢ u_{1} ⟶ u′_{1} s ⊢ u_{2} ⟶ u′_{2}}{s ⊢ u_{1} + u_{2} ⟶ u′_{1} + u′_{2}} \frac{s ⊢ u_{1} ⟶ u′_{1} s ⊢ u_{2} ⟶ u′_{2}}{s ⊢ u_{1} u_{2} ⟶ u′_{1} u′_{2}}

where y ∉ u indicates that the variable y does not occur (free or bound) in the expression u.

Two closed terms u_{1} and u_{2} are α-congruent in the traditional sense [1, page 26] if they are related by ∅ ⊢ u_{1} ⟶ u_{2}.

Definition 6. Given a translation context Ξ we define a substitution Ξ^{S} and an environment Ξ^{E} such that if fresh(n) = g then

(1) (Ξ[x : (σ, n)])^{S} = Ξ^{S}[x ↦ g]

(2) (Ξ[x : (σ, n)])^{E} = Ξ^{E}[x ↦ λz.up(VAR(g))]

If an object-language term u can be translated to a meta-language expression e then e will evaluate to a representation of u (modulo renaming).

Lemma 11. For any integer n, term u, expression e, type σ, and translation context Ξ with range(Ξ) = {(σ, i) | i < n}, if n; Ξ ⊢ u : σ / e then there exists a term u′ such that Ξ^{S} ⊢ u ⟶ u′ and [[e]]_{I_{0}} Ξ^{E} (up(n)) = up ⌈u′⌉.

Proof. By induction on the derivation of n; Ξ ⊢ u : σ / e.

Case n; Ξ ⊢ i : Int / int i. Then [[int i]]_{I_{0}} Ξ^{E} (up(n)) = up(INT (i)) = up ⌈i⌉

and indeed Ξ^{S} ⊢ i ⟶ i. Case n; Ξ ⊢ u_{1} + u_{2} : Int / add e_{1} e_{2} where n; Ξ ⊢ u_{1} : Int / e_{1} and n; Ξ ⊢ u_{2} :

Int / e_{2}. Then by two applications of the induction hypothesis there exist u′_{1} and u′_{2} such that Ξ^{S} ⊢ u_{1} ⟶ u′_{1}, Ξ^{S} ⊢ u_{2} ⟶ u′_{2}, [[e_{1}]]_{I_{0}} Ξ^{E} (up(n)) = up ⌈u′_{1}⌉, and [[e_{2}]]_{I_{0}} Ξ^{E} (up(n)) = up ⌈u′_{2}⌉. We therefore have

[[add e_{1} e_{2}]]_{I_{0}} Ξ^{E} (up(n))
= ADD_{⊥}([[e_{1}]]_{I_{0}} Ξ^{E} (up(n)), [[e_{2}]]_{I_{0}} Ξ^{E} (up(n)))_{⊥}
= ADD_{⊥}(up ⌈u′_{1}⌉, up ⌈u′_{2}⌉)_{⊥}
= up(ADD(⌈u′_{1}⌉, ⌈u′_{2}⌉))
= up ⌈u′_{1} + u′_{2}⌉

and indeed Ξ^{S} ⊢ u_{1} + u_{2} ⟶ u′_{1} + u′_{2}. Case n; Ξ ⊢ x : σ / x where Ξ(x) = (σ, m). Then, with g = fresh(m),

[[x]]_{I_{0}} Ξ^{E} (up(n)) = Ξ^{E}(x) (up(n)) = up(VAR(g)) = up ⌈g⌉
and indeed Ξ^{S} ⊢ x ⟶ g.

Case n; Ξ ⊢ λx.u : σ_{1} → σ_{2} / lam_{σ_{1},σ_{2}} (λx.e) where n + 1; Ξ[x : (σ_{1}, n)] ⊢ u : σ_{2} / e. Then with g = fresh(n), we have from the induction hypothesis that there exists u′ such that Ξ[x : (σ_{1}, n)]^{S} ⊢ u ⟶ u′. Definition 6(1) then gives Ξ^{S}[x ↦ g] ⊢ u ⟶ u′. Together with Definition 6(2) the induction hypothesis also gives

[[λx.e]]_{I_{0}} Ξ^{E} (up(n)) = LAM_{⊥}(up(g), [[e]]_{I_{0}} Ξ[x : (σ_{1}, n)]^{E} (up(n + 1)))_{⊥}
= LAM_{⊥}(up(g), up ⌈u′⌉)_{⊥}
= up(LAM (g, ⌈u′⌉)
= up ⌈λg.u′⌉

Since range(Ξ) ⊆ {(σ, i) | i < n} we have that for all z, Ξ^{S}(z) ≠ g. Hence

indeed Ξ^{S} ⊢ λx.u ⟶ λg.u′.

Case n; Ξ ⊢ u_{1} u_{2} : σ_{2} / app_{σ_{1},σ_{2}} e_{1} e_{2} where n; Ξ ⊢ u_{1} : σ_{1} / e_{1} and n; Ξ ⊢ u_{2} : σ_{1} → σ_{2} / e_{2}. (Follows the same structure as the case for addition.) Then by induction hypothesis there exist u′_{1} and u′_{2} such that Ξ^{S} ⊢ u_{1} ⟶ u′_{1}, Ξ^{S} ⊢ u_{2} ⟶ u′_{2}, [[e_{1}]]_{I_{0}} Ξ^{E} (up(n)) = up ⌈u′_{1}⌉, and [[e_{2}]]_{I_{0}} Ξ^{E} (up(n)) = up ⌈u′_{2}⌉. We therefore have

[[app_{σ_{1},σ_{2}} e_{1} e_{2}]]_{I_{0}} Ξ^{E} (up(n))
= APP_{⊥}([[e_{1}]]_{I_{0}} Ξ^{E} (up(n)), [[e_{2}]]_{I_{0}} Ξ^{E} (up(n)))_{⊥}
= APP_{⊥}(up ⌈u′_{1}⌉, up ⌈u′_{2}⌉)_{⊥}
= up(APP(⌈u′_{1}⌉, ⌈u′_{2}⌉))
= up ⌈u′_{1} u′_{2}⌉

and indeed Ξ^{S} ⊢ u_{1} u_{2} ⟶ u′_{1} u′_{2}.

Theorem 2 (Completeness). Given an object-language term u, if, for some σ, ∅ ⊢ u : σ then there exists an expression e with ∅ ⊢_{Σ_{0}} e : Exp σ and [[e]]_{I_{0}} ∅ (up(0)) = up ⌈u′⌉ for some u′ with ∅ ⊢ u ⟶ u′.

Proof. The term u must be closed. Hence, by Lemma 9, there exists an expression e with 0; ∅ ⊢ u : σ / e. This e is the candidate we’re seeking. Indeed, from Lemma 10, ∅ ⊢_{Σ_{0}} e : Exp σ and, from Lemma 11, there exists a term u′ with [[e]]_{I_{0}} ∅ (up(n)) = up ⌈u′⌉ and ∅ ⊢ u ⟶ u′.

4 Haskell as a meta-language

There are a number of issues that must be addressed to use Haskell as a metalanguage for embedded languages. Differences between Haskell and the idealized meta-language presented in the previous section influence the conditions under which Haskell can safely be used as a meta-language.

There are no built-in types Exp σ or constant symbols lam_{σ_{1},σ_{2}} and app_{σ_{1},σ_{2}} in Haskell. Instead, we must provide global definitions as in Figure 2 and argue that their semantics agree with the semantics of lam_{σ_{1},σ_{2}} and app_{σ_{1},σ_{2}}. We have designed the semantics of these constant symbols to match the Haskell implementation. Furthermore, in Haskell, the types of these symbols are restricted outside the module of their implementation. In contrast, in the formal development they are given as constant symbols of the restricted types.

The formal treatment in this work uses strict data type constructors. In contrast, Haskell’s constructors are non-strict. For the soundness result, the strict constructors guarantee that we only observe the types of “finite” objectlanguage terms. In Haskell, it is possible to observe the shape of “infinite” terms using the top-level read-eval-print loop. For example, the following well-typed Haskell expression uses recursion to build an infinite object-language term.

                   let f = lam ( x   app f x) in f

Its meaning is the representation of the limit of the chain of incomplete terms

⊥

   ⊑ LAM "x1" (APP ⊥ (VAR "x1"))
   ⊑ LAM "x1" (APP (LAM "x2" (APP ⊥ (VAR "x2"))) (VAR "x1"))

⊑ ⋯

where ⊥ denotes the bottom element of the CPO of (non-strict) data types. In a formal account for the soundness property using non-strict data types it may be desirable not to give types to such infinitely expanding terms. Instead, the soundness property might state that if a “finite” object-language term is denoted by an expression of type Exp σ then it has type σ.

Haskell’s function space is lifted, e.g. [[τ_{1} → τ_{2}]]_{I} = ([[τ_{1}]]_{I} →_{c} [[τ_{2}]]_{I})_{⊥}, allowing observing termination of expressions of higher types using the top-level read-eval-print loop. In contrast, in the idealized meta-language an expression of higher type is always applied so its termination behavior is never observed independently. Changing the semantics to account for Haskell-like lifted function spaces does not appear to introduce any difficulties in the soundness proof.

Finally, the approach to embedding languages into higher-order host languages presented above inherits the known problems of higher-order abstract syntax [22]. Most importantly, a higher-order abstract syntax does not admit a notion of case analysis. In order to make any use of constructed objectlanguage terms, the embedding we have presented directly represents terms using a first-order data type which can be printed as text. However, the standard function spaces of functional languages are generally too large for adequate higher-order abstract syntax. For example, the implementation in Figure 2 actually allows representations of “exotic terms”, such as the following expression

of type Exp (Int   Int).
           lam ( x   if show x = "a" then int 1 else int 2)

Although closed, this term does not correspond to any object-language term. Depending on the context, it may behave as either a 1 or x 2. Here we have used the overloaded Haskell function show to obtain a representation of an object-language term as a string. Such show-like functions are not, however, tied to Haskell’s overloading mechanism. They can be implemented in Haskell as well as in languages without overloading (such as ML [29]) as ordinary polymorphic functions of type Exp a String.

Research on higher-order abstract syntax alleviates these problems by restricting the function spaces of the meta-language using, e.g., modal logic [10]. In Haskell and ML-like languages, however, such a requirement cannot be enforced by the type system. In the presence of show-like functions, there are no ways around the problems of higher-order abstract syntax other than to informally require the programmer to only observe the behavior of closed objectlanguage terms. This requirement appears to match the typical use of embedded languages in existing applications.

Below, we briefly discuss the embedded type discipline in the context of extended object languages and in the context of extended meta-languages.

    -- Finite products
    pair :: Exp a    Exp b    Exp (a, b)
    pfst :: Exp (a, b)    Exp a
    psnd :: Exp (a, b)    Exp b
    -- Lists
    nil  :: Exp [a]
    cons :: Exp a    Exp [a]    Exp [a]
    hd   :: Exp [a]    Exp a
    tl   :: Exp [a]    Exp [a]
    -- Booleans
    tt   :: Exp Bool
    ff   :: Exp Bool
    ift  :: Exp Bool    Exp a    Exp a    Exp a
    iszero :: Exp Int    Exp Bool
    isnull :: Exp [a]    Exp Bool

Figure 3: Extended object language.

4.1 Extended object language

As already mentioned, other domain-specific types and operations are easily added to the object language. Figure 3 presents the types of operations on finite products, lists, and booleans. (The actual definition of these primitives are similar to those presented in Figure 2 and are left out for conciseness.) It is straightforward to extend the proof of soundness and completeness to also handle the extensions outlined here.

It is also possible to extend the object language with types that do not exist in the meta-language. For example,

   type Ref a = ()
   ref :: Exp a    Exp (Ref a)
   get :: Exp (Ref a)    Exp a
   set :: Exp (Ref a)    Exp a    Exp ()

declares the types of pointer-manipulating object-language functions in Haskell. (Appropriate values can be defined as in Figure 2.) Values of type Ref will never be constructed and therefore we can choose a minimal representation, here as the unit type (). A similar technique is used to integrate COM objects into Haskell [17].

The domain-specific operations on base types considered here (i.e., int, add, and the operations of the extended language in Figure 3) are meta-functions: they do not represent first-class functions in the object language. For example, there is no object-language equivalent of a first-class zero predicate. Indeed, Haskell rejects the expression cons iszero nil (an attempt to represent a singleton list of a zero predicate). A first-class zero predicate can be embedded by

  data Raw = ... | ISZERO'
  iszero' :: Exp (Int    Bool)
  iszero' =  E ( ns    ISZERO')
and used as in cons iszero' nil of type Exp [Int   Bool].

Since the object language is higher order we can also apply object-language β and η conversions at the meta-level. The two function compositions

  lam . app :: Exp (a    b)    Exp (a    b)
  app . lam :: (Exp a    Exp b)    Exp a    Exp b

are the extensional identity function on object-language functions, and the extensional identity function on meta-language functions. In fact, in the sense of binding-times and two-level coercions, the first composition coerces a dynamic function to static and back to dynamic again whereas the second composition coerces a static function to dynamic and back to static again, using two-level η-expansions [5]. Given, for example, a Haskell-like object language where the meta-language expression iszero E represents (e 0) (where E represents e) and the meta-language expression iszero' represents ( 0). (In Haskell, denotes structural equality.) In the meta-language we then have the (extensional) identities

  iszero  = app iszero'     -- of type Exp Int    Exp Bool
  iszero' = lam iszero      -- of type Exp (Int    Bool)

since (for the first equality) for any meta-language expression E of type Exp Int representing e, app iszero' E represents ( 0) e and (for the second equality) lam iszero' represents x x 0 and indeed e 0 and ( 0) e are semantically identical, as are ( 0) and x x 0.

As opposed to Haskell, the object-language does not provide polymorphism and recursion. Polymorphic or recursive meta-language expressions that are accepted by Haskell’s type system are unfolded in the object language. For example, it is possible to define polymorphic representations of object-language values in the meta-language as illustrated above for finite products and lists. Even though we cannot represent object-language term such as

                   let f =  x   x in (f 0, f True)

we can inline let-bound polymorphic values in the object-language term. For example, the following expression has type Exp (Int, Bool).

        let f = lam( x   x) in pair (app f (int 0)) (app f tt)

It evaluates to the object-language term (( a a) 0, ( a a) True).

4.2 Extended meta-language

It is possible to extend the meta-language with other base types, finite products, and lists à la Haskell, and also to extend the proofs of soundness and completeness.

It is also possible to change the evaluation strategy of the meta-language to call-by-value. Adding other effects than non-termination, however, might give an unsound embedding. This is the case for ML [29]. Using assignments, for example, some well-typed ML expressions do not represent well-typed objectlanguage terms. In fact, as the following example shows, some expressions do not even yield representations of closed terms.

   let val v = ref (int 0)
   in  lam (fn x ⇒ (v := x; x));
       v
   end

This expression returns whatever symbolic variable was generated at the time of constructing the object-language lambda. This problem is due to the use of higher-order abstract syntax, not to the typed embedding.

5 Related work

The soundness proof presented in this article uses a Kripke logical relation. The development is akin to Filinski’s proof that type-directed partial evaluation implements a normalization function [16]. A corollary of Filinski’s work is that type-directed partial evaluation is type preserving, a result we have also established using the typed embedded language described in this work [6, 7].

Completeness could also be stated by giving a semantics of the object language and then showing that a term and its encoding are semantically equivalent. Our proof is stronger in that it shows that a term and its encoding are syntactically equal modulo renaming of bound variables. It also avoids dealing with the semantics of the object language.

Yelland has used Haskell as a meta-language for hosting stack instructions for a core Java Virtual Machine [48]. In his work, the type of a stack cell is parameterized by its contents using a phantom type. Essentially, instructions are given types that reflect their behavior on the stack. Yelland proves a soundness result stating that instructions that are well-typed in Haskell will not err on execution. In Yelland’s work, the object language is first order and has no notion of variables and bindings. Hence, he avoids higher-order abstract syntax. In contrast, we have considered a higher-order object language is this present work.

Phantom types provide a simple form of dependent types for constructing representations of simply-typed terms in Haskell. The embedding is limited, however, in that it does not allow a type-preserving deconstruction of simplytyped terms. This is partly due to the lack of higher-order matching in Haskell.

A dependently typed language, such as Martin-Löf’s type theory [31], can directly express both type-safe construction and deconstruction of object-language terms. Previously, Yang has shown how to encode another class of dependently typed expressions in ML [46, 47].

There exists a number of logical frameworks that specifically, although not exclusively, address the problem of manipulating typed higher-order objectlanguage terms [4, 12, 18, 19, 20, 21, 32, 34, 36]. Compared to Haskell, these languages typically provide a richer dependent-type system and a better support for higher-order abstract syntax via higher-order unification and matching. These logical frameworks are primarily aimed at reasoning about objectlanguage terms and, in some cases, also entire logics. In contrast, we have explored the extent to which general-purpose languages such as Haskell are adequate for hosting typed object languages.

In the mid-1980’s, Wand has defined the meaning of an object language (with primitive I/O and non-local jumps) in terms of the λ-calculus, viewing the latter as a semantic meta-language [44]. His translation is sound and complete in the sense that exactly the well-typed object-language terms have a welltyped meta-language counterpart. Thus, it can be seen as providing both a static and a dynamic semantics for the object language. (In fact, since the translated terms are in continuation-passing style, Wand also shows that the CPS transformation preserves well-typedness [28].) Wand’s translation does not yield first-order data as result such as the embedding we consider here. Instead, it maps higher-order functions to higher-order functions. Furthermore, Wand’s object-language type system is not presented in terms of his meta-language. In contrast, the embedded type discipline we consider here expresses the type system of the object language in terms of the type system of the meta-language (using phantom types).

Davies’s λ^{◯}-calculus is an extension of the simply-typed λ-calculus for expressing staged evaluation [8]. In λ^{◯}, a term of type ◯σ evaluates in one stage to a value representing a term of type σ. Terms of type ◯σ are thus first-class representations of terms, much as the expressions of type Exp σ in our work are representations of object-language terms. There is a syntactic difference, however. In λ^{◯} there is one uniform construct for building terms at the next stage. The meta-language in our work provides several constructors, one for each syntactic category of the object language. (Analogy: λ^{◯} provides a type system for Lisp-like quasiquotation [2] whereas phantom types provide a type system for ML-like data types.) Another difference is that λ^{◯}-terms build other λ^{◯}- terms for a later stage. In contrast, the object-language terms in our work are always simply typed λ-terms. Consequently, we cannot embed object languages with an arbitrary number of stages. There is some hope, though, that type encodings as described by Yang [46] could achieve such a nested embedding, a staged version of which is provided in a language such as MetaML [43]. There is a growing interest in such statically typed, multi-stage languages because they provide a foundation for multi-stage evaluation and run-time code generation.

6 Conclusions

Phantom types make it possible to embed not only the (abstract) syntax but also the type system of a monomorphic object language into a statically typed meta-language such as Haskell. They have been used to design embedded languages [17, 25, 27] and to prove properties of programs [6, 7]. An experiment with run-time code generation for the rewrite engine of the logical framework MetaPRL [20] also confirms the utility of phantom types in a two-stage language [38, 39]. In this article, we have formally proved that phantom types yield sound and complete embeddings into an idealized meta-language and we have discussed the power and limitations of Haskell as such a meta-language.

Acknowledgements: I sincerely thank Olivier Danvy, Andrzej Filinski, Helmut Schwichtenberg, and Peter Sestoft for providing insightful comments on this work and Mikkel N. Hansen and Lasse R. Nielsen for kindly proof-reading earlier versions of this article. I am also grateful to the referees for their constructive comments and suggestions.

References

[1] Henk Barendregt. The Lambda Calculus — Its Syntax and Semantics. North-Holland, 1984.

[2] Alan Bawden. Quasiquotation in Lisp. In Olivier Danvy, editor, Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, number NS–99–1 in BRICS Note Series, pages 4–12, San Antonio, Texas, January 1999.

[3] William E. Carlson, Paul Hudak, and Mark P. Jones. An experiment using Haskell to prototype ‘geometric region servers’ for navy command and control. Technical Report 1031, Yale University, New Haven, Connecticut, November 1993.

[4] Robert L. Constable, Stuart F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, 1986.

[5] Olivier Danvy, Karoline Malmkjær, and Jens Palsberg. Eta-expansion does The Trick. ACM Transactions on Programming Languages and Systems, 8(6):730–751, 1996.

[6] Olivier Danvy and Morten Rhiger. A simple take on typed abstract syntax in Haskell-like languages. In Herbert Kuchen and Kazunori Ueda, editors, Proceedings of the Fifth International Symposium on Functional and Logic Programming, number 2024 in Lecture Notes in Computer Science, pages 343–358, Tokyo, Japan, March 2001. Springer-Verlag. An extended version is available as the technical report BRICS RS-00-34.

[7] Olivier Danvy, Kristoffer Høgsbro Rose, and Morten Rhiger. Normalization by evaluation with typed abstract syntax. Journal of Functional Programming, 11(6):673–680, 2001. An extended version is available as the technical report BRICS RS-01-16.

[8] Rowan Davies. A temporal-logic approach to binding-time analysis. In Edmund M. Clarke, editor, Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 184–195, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.

[9] N. G. de Bruijn. Lambda calculus notation with nameless dummies. A tool for automatic formula manipulation with application to the Church-Rosser theorem. Indagationes Mathematicae, 34:381–392, 1972.

[10] Jöelle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. In P. de Groote and J. R. Hindley, editors, Proceedings of the 3rd International Conference on Typed Lambda Calculi and Applications, number 1210 in Lecture Notes in Computer Science, pages 147–163, Nancy, France, April 1997.

[11] Premkumar Devanbu and Jeff Poulin, editors. Proceedings of the Fifth International Conference on Software Reuse, Victoria, British Columbia, June 1998. IEEE Computer Society Press.

[12] Gilles Dowek, Amy Felty, Hugo Herbelin, Gerard Huet, Chet Murthy, Catherine Parent, Christine Paulin-Mohring, and Benjamin Werner. The COQ proof assistant user’s guide. Technical Report 154, INRIA, Rocquencourt, France, 1993.

[13] Conal Elliott. Modeling interactive 3D and multimedia animation with an embedded language. In Chris Ramming, editor, First Conference on Domain-Specific Languages, pages 285–296, Santa Barbara, California, October 1997.

[14] Conal Elliott, Sigbjorn Finne, and Oege de Moor. Compiling embedded languages. In Walid Taha, editor, Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation, number 1924 in Lecture Notes in Computer Science, pages 9–27, Montréal, Canada, September 2000.

[15] Joseph H. Fasel, Paul Hudak, Simon Peyton Jones, and Philip Wadler. Haskell special issue. SIGPLAN Notices, 27(5), May 1992.

[16] Andrzej Filinski. A semantic account of type-directed partial evaluation. In Gopalan Nadathur, editor, International Conference on Principles and Practice of Declarative Programming, number 1702 in Lecture Notes in Computer Science, pages 378–395, Paris, France, September 1999. Springer-Verlag.

[17] Sigbjorn Finne, Daan Leijen, Erik Meijer, and Simon Peyton Jones. Calling hell from heaven and heaven from hell. In Peter Lee, editor, Proceedings of the 1999 ACM SIGPLAN International Conference on Functional Programming, pages 114–125, Paris, France, September 1999. ACM Press.

[18] Michael J. C. Gordon and Tom Melham. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993.

[19] Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, 1993. A preliminary version appeared in the proceedings of the First IEEE Symposium on Logic in Computer Science, pages 194–204, June 1987.

[20] Jason Hickey. Metaprl homepage. http://metaprl.org.

[21] Jason Hickey. Nuprl-light: An implementation framework for higher-order logics. In William McCune, editor, 14th International Conference on Automated Deduction, number 1249 in Lecture Notes in Artificial Intelligence, pages 395–399. Springer-Verlag, 1997.

[22] Martin Hofmann. Semantical analysis of higher-order abstract syntax. In Giuseppe Longo, editor, Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 1999. IEEE Computer Society Press.

[23] Paul Hudak. Modular domain specific languages and tools. In Devanbu and Poulin [11], pages 134–142.

[24] Paul Hudak, Tom Makucevich, Syam Gadde, and Bo Whong. Haskore music notation – an algebra of music. Journal of Functional Programming, 6(3):465–483, 1996.

[25] Simon Peyton Jones, Erik Meijer, and Daan Leijen. Scripting COM components in Haskell. In Devanbu and Poulin [11], pages 224–233.

[26] Peter J. Landin. The next 700 programming languages. Communications of the ACM, 9(3):157–166, 1966.

[27] Daan Leijen and Erik Meijer. Domain specific embedded compilers. In Thomas Ball, editor, Proceedings of the 2nd USENIX Conference on Domain-Specific Languages, pages 109–122, 1999.

[28] Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambda-calculi (summary). In Rohit Parikh, editor, Logics of Programs – Proceedings, number 193 in Lecture Notes in Computer Science, pages 219–224, Brooklyn, June 1985. Springer-Verlag.

[29] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). The MIT Press, 1997.

[30] John C. Mitchell. Type systems for programming languages. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, chapter 8, pages 365–458. The MIT Press, 1990.

[31] Bengt Nordström, Kent Petersson, and Jan Smith. Programming in Martin-Löf’s Type Theory. International Series on Monographs on Computer Science No. 7. Oxford University Press, 1990.

[32] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in Lecture Notes in Computer Science. Springer-Verlag, 1994.

[33] John Peterson, Paul Hudak, and Conal Elliott. Lambda in motion: Controlling robots with Haskell. In Gopal Gupta, editor, Proceedings of the First International Symposium on Practical Aspects of Declarative Languages, number 1551 in Lecture Notes in Computer Science, pages 91–105, San Antonia, Texas, January 1999. Springer-Verlag.

[34] Frank Pfenning. Logic programming in the LF logical framework. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 149–181. Cambridge University Press, 1991.

[35] Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Mayer D. Schwartz, editor, Proceedings of the ACM SIGPLAN’88 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 23, No 7, pages 199–208, Atlanta, Georgia, June 1988. ACM Press.

[36] Frank Pfenning and Carsten Schürmann. System description: Twelf — A meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), volume 1632 of Lecture Notes in Artificial Intelligence, pages 202–206, Trento, Italy, 1999. Springer-Verlag.

[37] Alastair Reid, John Peterson, Greg Hager, and Paul Hudak. Prototyping real-time vision systems: An experiment in DSL design. In Twenty-First International Conference on Software Engineering, pages 484–493, Los Angeles, California, May 1999. ACM Press.

[38] Morten Rhiger. Higher-Order Program Generation. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001.

[39] Morten Rhiger. Compiling embedded programs to byte code. In Shriram Krishnamurthi and C.R. Ramakrishnan, editors, Proceedings of the Fourth International Symposium on Practical Aspects of Declarative Languages, number 2257 in Lecture Notes in Computer Science, pages 120–136, Portland, Oregon, January 2002. Springer-Verlag.

[40] Dana Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 121:411–440, 1993.

[41] Guy L. Steele Jr. Growing a language. Higher-Order and Symbolic Computation, 12(3):221–236, October 1999.

[42] Joseph E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. The MIT Press, 1977.

[43] Walid Taha, Zine-El-Abidine Benaissa, and Tim Sheard. Multi-stage programming: Axiomatization and type safety. In Kim G. Larsen, Sven Skyum, and Glynn Winskel, editors, Proceedings of the 25th International Colloquium on Automata, Languages, and Programming, number 1443 in Lecture Notes in Computer Science, pages 918–929. Springer-Verlag, 1998.

[44] Mitchell Wand. Embedding type structure in semantics. In Mary S. Van Deusen and Zvi Galil, editors, Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 1–6. ACM Press, January 1985.

[45] Glynn Winskel. The Formal Semantics of Programming Languages. Foundation of Computing Series. The MIT Press, 1993.

[46] Zhe Yang. Encoding types in ML-like languages. In Paul Hudak and Christian Queinnec, editors, Proceedings of the 1998 ACM SIGPLAN International Conference on Functional Programming, pages 289–300, Baltimore, Maryland, September 1998. ACM Press. Extended version available as the technical report BRICS RS-98-9.

[47] Zhe Yang. Language Support for Program Generation: Reasoning, Implementation, and Applications. PhD thesis, Computer Science Department, New York University, New York, New York, August 2001.

[48] Phillip M. Yelland. A compositional account of the Java Virtual Machine. In Alex Aiken, editor, Proceedings of the Twenty-Sixth Annual ACM Symposium on Principles of Programming Languages, pages 57–69, San Antonio, Texas, January 1999. ACM Press.

Recent BRICS Report Series Publications

RS-02-34 Morten Rhiger. A Foundation for Embedded Languages. August 2002. 29 pp.

RS-02-33 Vincent Balat and Olivier Danvy. Memoization in Type-Directed Partial Evaluation. July 2002. 18 pp. To appear in Batory and Consel, editors, ACM SIGPLAN/SIGSOFT Conference on Generative Programming and Component Engineering, GPCE ’02 Proceedings, LNCS, 2002.

RS-02-32 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. On Obtaining Knuth, Morris, and Pratt’s String Matcher by Partial Evaluation. July 2002. 43 pp. To appear in Chin, editor, ACM SIGPLAN ASIAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, ASIA-PEPM ’02 Proceedings, 2002.

RS-02-31 Ulrich Kohlenbach and Paulo B. Oliva. Proof Mining: A Systematic Way of Analysing Proofs in Mathematics. June 2002. 47 pp.

RS-02-30 Olivier Danvy and Ulrik P. Schultz. Lambda-Lifting in Quadratic Time. June 2002.

RS-02-29 Christian N. S. Pedersen and Tejs Scharling. Comparative Methods for Gene Structure Prediction in Homologous Sequences. June 2002. 20 pp.

RS-02-28 Ulrich Kohlenbach and Laurenţiu Leuştean. Mann Iterates of Directionally Nonexpansive Mappings in Hyperbolic Spaces. June 2002. 33 pp.

RS-02-27 Anna Östlin and Rasmus Pagh. Simulating Uniform Hashing in Constant Time and Optimal Space. 2002. 11 pp.

RS-02-26 Margarita Korovina. Fixed Points on Abstract Structures without the Equality Test. June 2002.

RS-02-25 Hans Hüttel. Deciding Framed Bisimilarity. May 2002. 20 pp.

RS-02-24 Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Static Analysis for Dynamic XML. May 2002. 13 pp.

RS-02-23 Antonio Di Nola and Laurenţiu Leuştean. Compact Representations of BL-Algebras. May 2002. 25 pp.