Mixed Inductive/Coinductive Types and Strong Normalization

Andreas Abel^{⋆}

Department of Computer Science, University of Munich Oettingenstr. 67, D-80538 München, Germany

                         andreas.abel@ifi.lmu.de

Abstract. We introduce the concept of guarded saturated sets, saturated sets of strongly normalizing terms closed under folding of corecursive functions. Using this tool, we can model equi-inductive and equicoinductive types with terminating recursion and corecursion principles. Two type systems are presented: Mendler (co)iteration and sized types. As an application we show that we can directly represent the mixed inductive/coinductive type of stream processors with associated recursive operations.

1 Introduction

Symbolic evaluation, aka evaluation of terms with free variables, is used, amongst others, for optimization through partial evaluation in compilers and for checking term equivalence in languages based on dependent types—such as the theorem provers Agda, Coq, Epigram, and LEGO, founded on intensional type theory. In these applications, symbolic evaluation is required to terminate. My long term research goal is to develop expressive type systems that guarantee termination, and these type system shall include inductive and coinductive types.

Most research on inductive types has focused on the iso-style, i. e., there are explicit operations in : F (μF) → μF and out : μF → F (μF) for wrapping and unwrapping inductive types. In contrast, equi-inductive types come with the type equation μF = F (μF), so wrapping and unwrapping is silent on the term level. Recently [4], I have put forth a type system for strongly normalizing terms with equi-(co)inductive types, but it behaves badly for so-called mixed inductive/coinductive types.

However, mixed inductive/coinductive types are important in the context of intensional type theory. Ghani, Hancock, and Pattinson [10] show how the type νX. μY. (B×X)+(A → Y) of stream processors is inhabited by codes of functions from streams over A to streams over B. They define eating, a function which takes a stream processor and an input stream and produces an output stream; eating executes the code of a stream processor. Swierstra [17] demonstrated how a small modification of stream processors could be used to model I/O in a dependently typed programming language.

⋆ Research partially supported by the EU coordination action TYPES (510996).

In this article, I present a concept which paves the way to a satisfactory treatment of mixed equi-(co)inductive types: guarded type expressions. The term guardedness has been used as a criterion whether corecursive programs denote well-defined functions. A corecursive call is guarded if it appears under a constructor of the coinductive type. In the same sense, a type expression is guarded if it is headed by a proper type constructor, like function space, cartesian product, disjoint sum, or a primitive type. Using the guardedness criterion, we can avoid coinductive types which contain no weak head values, and the remaining coinductive types have the pleasant property that they already contain a corecursive value if they contain its unfolding. This property gives rise to the new concept of guarded saturated set, on which we base our normalization proof.

Related Work. There is a rich body of work on type systems for termination of recursion, starting with Mendler [12], with contributions by Amadio and Coupet-Grimal [6], a group around Giménez and Barthe [7, 8], and Blanqui and Riba [9]. All of these works are concerned with iso-(co)inductive types. Parigot [13] introduces equi-inductive and coinductive types in second-order functional arithmetic, an extension of System F. [15] provides Mendler iteration and coiteration schemes for these types and proves that all well-typed terms are hereditarily solvable, if the involved types satisfy a certain strictness condition. We require a condition only on coinductive types. Hughes, Pareto, and Sabry [11] present sized types in the equi-style, yet they consider only finitely branching data types and explicitly exclude a type of stream processors. In my previous attempt at equi-(co)inductive types [4] I constructed a semantics based on biorthogonals, which are due to Girard and have been successfully applied at interpreting languages based on classical logic (see, e. g., Parigot [14]). However, I had to consider a recursive function applied to a corecursive value blocked, preventing the use of mixed inductive/coinductive types. In this article, this flaw is overcome by a semantics based on saturated sets.

Overview. In Sec. 2, we will see a λ-calculus with recursion and corecursion and a saturated-set semantics of strongly normalizing terms. On this semantics, we base first a type system with Mendler (co)iteration (Sec. 3), and then a more flexible one with sized types (Sec. 4).

2 Untyped Language and Semantics

As an idealized purely functional programming language, we consider the λcalculus with pairs and projections, injections and case analysis, and recursion and corecursion. In this section, we define semantical types as sets of strongly normalizing terms and prove formation, introduction and elimination rules for these semantical types. Especially interesting will be the principles for terminating recursion and corecursion which will be derived from the construction of inductive and coinductive types by ordinal iteration.

In all expressions throughout this article a dot “.” denotes an opening parenthesis closing as far to the right as syntactically meaningful. [M/x]N denotes the capture avoiding substitution of M for x in N. Let x range over a countably infinite set Var of variables. We define our language as the lambda calculus equipped with constants c. The values v are λ-abstractions, pairs, injections, and not fully applied constants (including recursive functions and corecursive values).

c  ::= () | pair | fst | snd | inl | inr | case
| fix^{μ} | fix_{n}^{ν} (n ∈ ℕ) constants
r, s, t ::= c | x | λxt | r s  terms
v, w ::= c | λxt | pair r | pair r s | inl r | inr r
| fix^{μ} s | fix_{n}^{ν}s t (|t| ≤ n)  (weak-head) values
e^{−}( ) ::= s | fst | snd | case s t  non-recursive evaluation frames
e( ) ::= e^{−}( ) | fix^{μ} s  evaluation frames
E( ) ::= | E(e( ))  evaluation contexts.

We distinguish between possibly recursive e( ) and non-recursive e^{−}( ) evaluation frames. An evaluation context is E( ) is a stack of evaluation frames. Corecursive functions are only unfolded in a non-recursive evaluation frame

Reduction. Computation is modeled as small-step reduction relation. These are the axioms of β-contraction e(v) ↣ t.

(λxt) s  ↣ [s/x]t
fix^{μ} s v  ↣ s (fix^{μ} s) v
e^{−}(fix_{n}^{ν} s t_{1..n}) ↣ e^{−}(s (fix_{n}^{ν} s) t_{1..n})

fst (pair r s) ↣ r
snd (pair r s) ↣ s
case (inl r) s t ↣ s r
case (inr r) s t ↣ t r

One-step reduction ⟶ is the closure of ↣ under all term constructors, multistep reduction ⟶^{+} its transitive closure and ⟶^{∗} its reflexive-transitive closure. Weak head reduction is defined by E(t) ⟶_{w} E(t′) ⟺ t ↣ t′.

By only unfolding corecursive values in non-recursive evaluation frames, we avoid critical pairs. This does not lead to stuck terms, since in such a case the recursive function constituting the frame can be unfolded instead. In previous work [4], we considered a corecursive value in a recursive frame as stuck, leading to an unsatisfactory treatment of mixed induction/coinduction. The present work overcomes this flaw.

Strong normalization and saturated sets. A term t is strongly normalizing (s.n.), written t ∈ SN, if all reduction sequences starting with t are finite. Note that subterms and reducts of s.n. terms are also s.n. Terms E(x) ∈ SN are called s.n. and neutral and their collection is denoted by SNe.

A set of terms A is a semantical type, written A ∈ SAT_{u}, if

1. SNe ⊆ A ⊆ SN,

2. each term in A weak-head reduces either to a value or a neutral term,

3. A is closed under weak head expansion that does not introduce diverging terms.

The first condition ensures that each semantical type contains all variables, such that we can construct an open s.n. term model of our calculus. The second condition is used to justify recursive functions fix^{μ} s, which reduce under callby-(weak-head)-value (see Lemma 3). The third condition ensures that a redex like (λxt) s inhabits a semantical type if its reduct (here [s/x]t) does so. This is needed, for instance, to establish that λxt is in the semantical function space, and similarly for pair r s, case distinctions and recursive functions.

The third condition can be made precise by defining safe weak head reduction, ▷, by the following rules:

(λxt) s  ▷ [s/x]t  if s ∈ SN
fix^{μ} s v  ▷ s (fix^{μ} s) v
e^{−}(fix_{n}^{ν} s t_{1..n}) ▷ e^{−}(s (fix_{n}^{ν} s) t_{1..n})
E(t)  ▷ E(t′)  if t ▷ t′

fst (pair r s) ▷ r if s ∈ SN
snd (pair r s) ▷ s if r ∈ SN
case (inl r) s t ▷ s r if t ∈ SN
case (inr r) s t ▷ t r if s ∈ SN

We define ▷ as the reflexive-transitive closure of the above rules. Now if t ▷ t′ ∈ SN, then t ∈ SN. For a reduction relation R, let ^{R}A := {t | t R t′ ∈ A} and A^{R} := {t′ | A ∋ t R t′}. Condition 3 of semantical types can then be written as ▷A ⊆ A.

The greatest semantical type is called S, it contains all s.n. terms except those whose weak-head reduction gets stuck, like fst (λxx). The least semantical type is N := ^{▷}SNe, and it is closed under s.n. evaluation contexts: if r ∈ N and E(x) ∈ SNe then E(r) ∈ N.

Guarded semantical types. A semantical type A is guarded, written A ∈ SAT_{g}, if s (fix_{n}^{ν} s) t_{1..n} ∈ A implies fix_{n}^{ν} s t_{1..n} ∈ A. Let ▶ ⊇ ▷ be the reflexive-transitive closure of safe weak head reduction plus the axiom

fix_{n}^{ν} s t_{1..n} ▶ s (fix_{n}^{ν} s) t_{1..n}.

Note that r ▶ r′ implies e^{−}(r) ▷ e^{−}(r′).

A semantical type A is guarded iff ^{▶}A ⊆ A. The premier example of a nonguarded type is N. Note that S is closed under ▶-expansion, since fix_{n}^{ν} s t_{1..n} is a strongly normalizing value if s, t_{1..n} ∈ SN. Thus, S is guarded.

Constructions on semantical types. The following constructions produce guarded semantical types, even for unguarded A, B ∈ SAT_{u}.

A → B := {r | r s ∈ B for all s ∈ A}
A × B := {r | fst r ∈ A and snd r ∈ B}
A + B := ^{▶}(inl(A) ∪ inl(B) ∪ SNe)
1  := ^{▶}({()} ∪ SNe)

Note that SAT_{g} and SAT_{u} are closed under arbitrary intersections and unions. The last property is the advantage of saturated-sets semantics, it does not always hold for candidates of reducibility or biorthogonals, and even when it holds the proof is non-trivial [16].

If F is a monotone operator on sets of terms, and α an ordinal, we define the term sets μ^{α}F and ν^{α}F by iteration on α as follows.

\begin{aligned}μ^{0} & F & := & N \\ μ^{α+1} & F & := & F(μ^{α}F) \\ μ^{λ} & F & := & ⋃_{α<λ} μ^{α}F \end{aligned}  \begin{aligned}ν^{0} & F & := & S \\ ν^{α+1} & F & := & F(ν^{α}F) \\ ν^{λ} & F & := & ⋂_{α<λ} ν^{α}F \end{aligned}

Herein, λ denotes limit ordinals > 0. Let ∞ denote the ordinal at which, for any F, iteration from below reaches the least fixed-point μ^{∞}F = F(μ^{∞}F), and iteration from above reaches the greatest fixed-point ν^{∞}F = F(ν^{∞}F). Since term sets are countable, ∞ is at most the first uncountable ordinal.

Now if F(A) is guarded for any A ∈ SAT_{u}, then μ^{α}F will be guarded for α ≥ 1. If F(A) is guarded for any guarded A, then ν^{α}F is guarded for all α.

Lemma 1 (Semantical formation). The following implications, written as rules, hold:

\frac{A, B ∈ SAT_{u}}{A ⋆ B ∈ SAT_{g}} ⋆ ∈ \{→, ×, +\}  \overline{1 ∈ SAT_{g}}  \overline{N ∈ SAT_{u}}  \overline{S ∈ SAT_{g}}

\frac{F ∈ SAT_{u} → SAT_{b}}{μ^{∞}F ∈ SAT_{b}} b ∈ \{u, g\} \frac{F ∈ SAT_{g} → SAT_{b}}{ν^{∞}F ∈ SAT_{b}} b ∈ \{u, g\}

Proof. We show the first implication, A → B ∈ SAT_{g}. It is sufficient to assume {x} ⊆ A ⊆ SN and B ∈ SAT_{u}. Let r ∈ A → B. First, r x ∈ B ⊆ SN by assumption, hence r ∈ SN. Second, we know that r x weak-head reduces to either a neutral term or a value. Hence, either r weak-head reduces to a neutral term, or to a λ-abstraction, which is a value. Third, let r′ ▶ r. Then for any s ∈ A we have r′ s ▷ r s which, since B ∈ SAT_{u}, implies r′ s ∈ B. This entails r′ ∈ A.

Lemma 2 (Semantical typing). The following implications hold:

\frac{[s/x]t ∈ B for all s ∈ A}{λxt ∈ A → B}  \frac{r ∈ A → B  s ∈ A}{r s ∈ B}

\frac{r ∈ A  s ∈ B}{pair r s ∈ A × B}  \frac{r ∈ A × B}{fst r ∈ A}  \frac{r ∈ A × B}{snd r ∈ B}  \overline{() ∈ 1}

\frac{t ∈ A}{inl t ∈ A + B}  \frac{t ∈ B}{inr t ∈ A + B}  \frac{r ∈ A + B  s ∈ A → C  t ∈ B → C}{case r s t ∈ C}

Proof. The rules for λ, pair, and case are proven by closure of saturated sets under safe weak head expansion. (The remaining rules hold already by definition.) We show the last implication. Assume r ∈ A+B, then r ▶ r′ where r′ is either neutral or a left or right injection. We observe that case r s t ▷ case r′ s t and distinguish the three cases: In the first case case r′ s t ∈ SNe, hence, case r s t ∈ N ⊆ C. In the second case, r′ = inl r′′ with r′′ ∈ A, thus, case r s t ▷ s r′′ ∈ C. The third case is analogous to the second.

The following semantical typing for recursion is the foundation of type-based termination à la Mendler [12], Amadio et al. [6] and Barthe et al. [7]. In a typical application of the following lemma, I(α) will be some inductive type μ^{α}F; then I(0) = N.

Lemma 3 (Recursion). For all ordinals α ≤ ∞ let I(α), C(α) ∈ SAT_{u} with I(0) ⊆ N. Set A(α) := I(α) → C(α) and stipulate continuity: ⋂_{α<λ} A(α) ⊆ A(λ) for all limit ordinals λ > 0. Then the following implication holds for all β ≤ ∞:

\frac{s ∈ ⋂_{α<∞} A(α) → A(α + 1)}{fix^{μ} s ∈ A(β)}.

Proof. By transfinite induction on β. The limit case is handled by the continuity condition on A. For the other cases, assume r ∈ I(β) and show fix^{μ} s r ∈ C(β). If r ∈ N then fix^{μ} s r ∈ N ⊆ C(β); since I(0) ⊆ N, this handles the case β = 0. Otherwise r ▷ v and β = α + 1 for some α. It is sufficient to show that the weak head reduct s (fix^{μ} s) v of fix^{μ} s r is in C(α + 1), but this follows from the induction hypothesis fix^{μ}s ∈ A(α) by the assumption s ∈ A(α) → A(α + 1).

The proof for β = 0 needs N to be closed under evaluation contexts, fix^{μ}s in our case. If N was also guarded, then fix_{0}^{ν}λ x ∈ N and fix^{μ}(λff)(fix_{0}^{ν}λ x) ∈ N, a diverging term. Thus, the least type needs to be classified as unguarded.

Remark 1 (Continuity). Let Nat^{α} = μ^{α}(X ↦ 1 + X) be the semantical type corresponding to the set of natural numbers < α. The function A(α) = (Nat^{ω} → Nat^{α}) → 1 violates the continuity condition: one can implement a test p(f) in our calculus that halts whenever it has found numbers n, m with f(n) = f(m). The test will halt for bounded functions f ∈ Nat^{ω} → Nat^{α} for α < ω, but diverges on, for example, any strictly monotone unbounded function f ∈ Nat^{ω} → Nat^{ω}. This justifies the necessity of the continuity condition for the soundness of our semantics [2].

The following lemma dualizes Lemma 3; it is tailored for guarded C(α) = ν^{α}F. To prove it, we have introduced the concept of guardedness in the first place.

Lemma 4 (Corecursion). For α ≤ ∞ let B_{1}(α), …, B_{n}(α) ∈ SAT_{u} and C(α) ∈ SAT_{g} such that S ⊆ C(0). Set A(α) := B_{1}(α) → ⋯ → B_{n}(α) → C(α) and stipulate ⋂_{α<λ} A(α) ⊆ A(λ) for limits λ. Then for all β ≤ ∞,

\frac{s ∈ ⋂_{α<∞} A(α) → A(α + 1)}{fix_{n}^{ν} s ∈ A(β)}.

Proof. By transfinite induction on β, limits again handled by continuity of A. Assume t_{i} ∈ B_{i}(β) for i = 1..n and show r := fix_{n}^{ν} s t_{1..n} ∈ C(β). In case β = 0 it is sufficient to show r ∈ S, but this holds since r is a value and its direct subterms are all s.n. In case β = α +1, observe that r ▶ s (fix_{n}^{ν} s) t_{1..n} ∈ C(α +1) by induction hypothesis fix_{n}^{ν} s ∈ A(α) and assumption s ∈ A(α) → A(α + 1). Since C(α + 1) is guarded, we are done.

We have identified semantically sound principles for recursion and corecursion. In the next sections, we implement two type systems on this basis.

3 A Basic Type System: Mendler (Co)Iteration

In this section, we consider a type system for iteration over equi-inductive types and coiteration over equi-coinductive types in the style of Mendler [12]. Mendler-iteration, like conventional iteration coming from initial algebra semantics, is usually formulated for iso-inductive types, with an explicit constructor in : F (μF) → μF. Our developments in the last section paved the way for equi-style formulations.

Types are given by the following grammar

\begin{aligned}⋆ & ::= & → | × | + \\ A, B, C & ::= & X | 1 | A ⋆ B | ∀XA | μXA | νXA. \end{aligned}

The type constructors ∀, μ, and ν bind variable X in A. The type μXX is an empty, unguarded type; we especially need to avoid unguarded coinductive types like νY μXX. To this end, we present a kinding judgement with two base kinds: ∗_{g}, guarded types, and ∗_{u}, unguarded types.

Let θ be a map from type variables to semantical types. We define the semantics [[A]]_{θ} of type A by recursion on A as follows:

[[X]]_{θ} = θ(X)_{[[A ⋆ B]]_{θ} = [[A]]_{θ} ⋆ [[B]]_{θ}}_{[[1]]_{θ} = 1} [[∀XA]]_{θ} = ⋂_{X ∈SAT_{u}}[[A]]_{θ[X↦X]}

[[μXA]]_{θ} = μ^{∞}(X ∈ SAT_{u} ↦ [[A]]_{θ[X↦X]})
[[νXA]]_{θ} = ν^{∞}(X ∈ SAT_{g} ↦ [[A]]_{θ[X↦X]})

Kinding. Let Δ be a finite map from type variables to base kinds. We write Δ, X : κ for the updated map Δ′ with Δ′(X) = κ and Δ′(Y) = Δ(Y) in case Y ≠ X. In the update operation, we presuppose X ∉ dom(Δ). The judgment Δ ⊢ A : κ is inductively given by the following rules (where b ∈ {u, g}).

\overline{Δ ⊢ X : Δ(X)}  \overline{Δ ⊢ 1 : ∗_{g}}  \frac{Δ ⊢ A : ∗_{g}}{Δ ⊢ A : ∗_{u}}  \frac{Δ ⊢ A : ∗_{u}  Δ ⊢ B : ∗_{u}}{Δ ⊢ A ⋆ B : ∗_{g}}

\frac{Δ, X:∗_{u} ⊢ A : ∗_{b}}{Δ ⊢ ∀XA : ∗_{b}}  \frac{Δ, X:∗_{u} ⊢ A : ∗_{b}}{Δ ⊢ μXA : ∗_{b}} pos  \frac{Δ, X:∗_{g} ⊢ A : ∗_{g}}{Δ ⊢ νXA : ∗_{g}} pos

In the formation rules for (co)inductive types we require (pos) that X appears only positively in A (otherwise, the denoted fixed-points might not exist).

The soundness of kinding is immediate. Let θ ∈ [[Δ]] iff Δ(X) = ∗_{b} implies θ(X) ∈ SAT_{b} for all X.

Theorem 1 (Soundness of kinding). If Δ ⊢ A : ∗_{b} and θ ∈ [[Δ]] then [[A]]_{θ} ∈ SAT_{b}.

Type equality. Let Δ ⊢ A = A′ be the least congruence over the two axioms

\frac{Δ ⊢ μXA : ∗_{u}}{Δ ⊢ μXA = [μXA/X]A} \frac{Δ ⊢ νXA : ∗_{g}}{Δ ⊢ νXA = [νXA/X]A}.

Lemma 5 (Soundness of type substitution and equality).

1. [[[B/X]A]]_{θ} = [[A]]_{θ[X↦[[B]]_{θ}]}.

2. If Δ ⊢ A = A′ and θ ∈ [[Δ]] then [[A]]_{θ} = [[A′]]_{θ}.

Typing. Let Γ be a finite map from type variables to kinds and term variables to types, with additional update operation Γ, x: A. Each Γ can be viewed as a Δ, by ignoring the term variable bindings. The typing judgement Γ ⊢ t : A is inductively given by the following rules:

\frac{Γ ⊢ Γ (x) : ∗_{u}}{Γ ⊢ x : Γ (x)}  \frac{Γ, x:A ⊢ t : B}{Γ ⊢ λxt : A → B}  \frac{Γ ⊢ r : A → B  Γ ⊢ s : A}{Γ ⊢ r s : B}

\frac{Γ, X:∗_{u} ⊢ t : A}{Γ ⊢ t : ∀XA}  \frac{Γ ⊢ t : ∀XA  Γ ⊢ B : ∗_{u}}{Γ ⊢ t : [B/X]A}  \frac{Γ ⊢ t : A  Γ ⊢ A = B}{Γ ⊢ t : B}

\overline{Γ ⊢ c : Σ(c)}  \frac{Γ ⊢ μXA : ∗_{u}  Γ ⊢ C : ∗_{u}}{Γ ⊢ fix^{μ} : (∀X. (X → C) → A → C) → μXA → C}

\frac{Γ ⊢ νXA : ∗_{g} Γ ⊢ B_{i} : ∗_{u} for i = 1..n}{Γ ⊢ fix_{n}^{ν} : (∀X. (B_{1..n} → X) → B_{1..n} → A) → B_{1..n} → νXA}

Herein, the signature Σ assigns the following types to constants c:

pair : ∀A∀B. A → B → A × B
fst : ∀A∀B. A × B → A
snd : ∀A∀B. A × B → B
() : 1

inl : ∀A∀B. A → A + B
inr : ∀A∀B. B → A + B
case : ∀A∀B∀C. A + B →
(A → C) → (B → C) → C

Example 1. If we drop the guardedness condition in the corecursion rule, then the diverging term fix^{μ}(λff) (fix_{0}^{ν}λ x) can be typed. First observe that fix^{μ}λff : μXX → C for any C. In the context x : μXX we have λ x : ∀Y. Y → μXX, hence, fix_{0}^{ν}λ x : νY μXX. With νY μXX = μXX we get the typing x: μXX ⊢ fix^{μ}(λff) (fix_{0}^{ν}λ x) : C. This demonstrates that guardedness is vital for the termination of open expressions when mixing recursion and corecursion. Nonemptiness is not necessary, however; an analogous term constructed with the empty, but guarded type νY. 1 → μXX is not diverging.

Let θ now be a finite map from type variables to semantical types and from term variables to terms. We write θ ∈ [[Γ]] if additionally to the condition on type variables θ(x) ∈ [[Γ (x)]]_{θ} for all term variables x ∈ dom(Γ). Let tθ denote the simultaneous (capture-avoiding) substitution of all x ∈ FV(t) by θ(x).

Theorem 2 (Soundness of typing). If Γ ⊢ t : A and θ ∈ [[Γ]] then tθ ∈ [[A]]_{θ}.

Proof. By induction on the typing derivation, using the result of the last section.

In case of fix^{μ}, assume s ∈ ⋂_{X ∈SAT_{u}}[[(X → C) → A → C]]_{θ[X↦X]} and show fix^{μ} s ∈ [[μXA → C]]_{θ}. Lemma 3 (recursion) is applicable with types I(α) = μ^{α}(X ↦ [[A]]_{θ[X↦X]}) and C(α) = [[C]]_{θ}. Since r ∈ I(λ) = ⋃_{α<λ} I(α) implies r ∈ I(α) for some α < λ and C does not depend on its ordinal argument, the continuity condition is trivially satisfied for A(α) = I(α) → C(α). For all α, the typing s ∈ A(α) → A(α + 1) requested by the lemma is an instance of the given typing with X = I(α), since [[A]]_{θ[X↦I(α)]} = I(α + 1).

In case of fix^{ν}, Lemma 4 is applicable, analogously to the case of fix^{μ}. The kinding ensures that C(α) := ν^{α}(X ↦ [[A]]_{θ[X↦X]}) is guarded for all α ≤ ∞. The continuity condition is again trivially satisfied.

Corollary 1 (Strong normalization and consistency). Each typable term is strongly normalizing. Each closed well-typed term weak-head reduces to a value. No closed term inhabits ∀XX.

Proof. By soundness of typing, letting θ(X) = N for all type variables X and θ(x) = x for all term variables x. Consistency, the last statement, follows since there are no closed terms in N.

Example: Stream Eating with Mendler (Co)Iteration

We first allow ourselves some syntactic sugar: we write (r, s) for pair r s and use matching abstraction λ(x, y).t as a shorthand for λz. [fst z/x][snd z/y]t. ML-style pattern matching match t with p_{i} ↦ t_{i} for patterns p_{i} composed from variables, (), pair, inl, and inr, can also be defined easily [5, Sec. 2.4].

To provide some help for type-checking (by the reader and by the machine), we sometimes will use Church-style syntax and allow type-annotations t : A in the example programs:

\frac{Γ ⊢ t : A}{Γ ⊢ (t : A) : A}  \frac{Γ, x:A ⊢ t : B}{Γ ⊢ λx:A. t : A → B}

\frac{Γ, X:∗_{u} ⊢ t : A}{Γ ⊢ ΛXt : ∀XA}  \frac{Γ ⊢ t : ∀XA  Γ ⊢ B : ∗_{b}}{Γ ⊢ t[B] : [B/X]A}

Streams Stream A := νX. A × X can be constructed by pair : ∀A.A → Stream A → Stream A and destructed by fst : ∀A. Stream A → A and snd : ∀A. Stream A → Stream A. In Haskell, stream processors are defined as a data type and the code of the mapping function is generally recursive.

    data SP a b where
      get :: (a -> SP a b) -> SP a b
      put :: b -> SP a b -> SP a b
    map :: (a -> b) -> SP a b
    map f = get (\ a -> put (f a) (map f))

In our system, we define the type of codes for stream processing functions [10] as a interleaved coinductive-inductive type.

SP A B := νXμY.B × X + (A → Y)

The equi-style enables a direct representation of the constructors:

put := inl : ∀A∀B. B × SP A B → SP A B
get := inr : ∀A∀B. (A → SP A B) → SP A B

The code of the stream-mapping function can be defined by Mendler coiteration as follows:

map : ∀A∀B. (A → B) → SP A B
map := ΛAΛBλf:A → B.

fix_{0}^{ν} ΛXλmap : X. inr (λa:A. inl (f a, map) : μY. B × X + (A → Y))

Stream eating executes the code of a stream processor, consuming an input stream and producing an output stream. In Haskell it is again defined by general recursion:

    eat :: SP a b -> [a] -> [b]
    eat (get f) (a:as) = eat (f a) as
    eat (put b t)  as  = b : eat t as

We define eating by an outer Mendler coiteration on the output stream and an inner Mendler iteration on the stream processor.

eat : SP A B → StreamA → StreamB
eat := fix_{2}^{ν} ΛXλeat^{ν}:SP A B → Stream A → X
fix^{μ} ΛY λeat^{μ}:Y → StreamA → B × X
λt:B × SP A B + (A → Y). λ(a, as). match t with
put (b, t′) ↦ (b, eat^{ν} t′ (a, as)) : B × X
get f  ↦ eat^{μ} (f a : Y) as

Some interesting functions, like composition of stream processors, are not (co)iterative, hence cannot be defined directly in the present type systems. Therefore, we introduce a more expressive system of sized types in the next section.

4 A Fancy Type System: Sized Types

Sized types allow a greater flexibility in defining recursive and corecursive functions by mapping the semantics more directly into the syntax of types. In the following, we describe an extension of the type system F^{ω} that makes the following features of semantics available in syntax:

1. Ordinals a and approximations μ^{a}F and ν^{a}F of inductive and coinductive types. The syntax of ordinals will be restricted to variables, successor and ∞. There is no need to provide notation for limit ordinals.

2. Distinction between guarded (∗_{g}) and unguarded types (∗_{u}). This feature is new in comparison to previous works [2, 8, 9].

3. Monotonicity information (polarity) of type constructors. For instance, the function space constructor is antitone in its first argument and monotone in its second argument, thus, it receives kind ∗_{u} →^{−} ∗_{u} →^{+} ∗_{g}. Using polarities, the positivity test for (co)inductive types scales to higher-orders [1].

Kinds classify type constructors. Besides ∗_{g} and ∗_{u} we introduce a kind ord_{u} of ordinals and a subkind ord_{g} ≤ ord_{u} of non-zero ordinals. Function kinds are annotated with a polarity p.

p, q ::= ∘  mixed-variant (no monotonicity information)
| +  covariant (monotone)
| −  contravariant (antitone)
| ⊤  constant (both mono- and antitone)
κ ::= ∗_{u} | ∗_{g} | ord_{u} | ord_{g} base kind
| κ →^{p} κ′  function kind

Subkinding κ ≤ κ′ is defined inductively by the following rules:

\overline{∗_{g} ≤ ∗_{u}}  \overline{ord_{g} ≤ ord_{u}}  \frac{κ′_{1} ≤ κ_{1}  p′ ≤ p  κ_{2} ≤ κ′_{2}}{κ_{1} →^{p} κ_{2} ≤ κ′_{1} →^{p′} κ′_{2}}

Herein, the order on polarities is the reflexive-transitive closure of the axioms ∘ ≤ p and p ≤ ⊤. If one composes a function in κ_{1} →^{p} κ_{2} with a function in κ_{2} →^{q} κ_{3} one obtains a function in κ_{1} →^{pq} κ_{3}. For the associative and commutative polarity composition pq we have the laws ⊤p = ⊤, ∘p = ∘ (for p ≠ ⊤), +p = p, and −− = +. Inverse application p^{−1}q of a polarity p to a polarity q is defined as the solution of

∀q, q′. p^{−1}q ≤ q′ ⟺ q ≤ pq′.

Type constructors F are type-level λ-terms over constants C:

\begin{aligned}C & ::= & → | × | + | 1 | ∀_{κ} | μ | ν | 0 | s | ∞ \\ A, B, F, G & ::= & C | X | λXF | F G \end{aligned}

We use →, ×, + infix and write ∀X:κ.A for ∀_{κ}λXA. If κ is ∗_{u}, it can be dropped. We write the ordinal argument a to μ and ν superscript, e.g., μ^{a}F.

Let Δ denote a finite map from type (constructor) variables X to pairs pκ of a polarity p and a kind κ. Inverse application p^{−1}Δ of a polarity p to Δ is defined by Δ(X) = qκ ⟹ (p^{−1}Δ)(X) = (p^{−1}q)κ. The following kinding rules [1] and kind assignments to constants handle polarities properly:

\frac{C : κ}{Δ ⊢ C : κ}  \frac{Δ(X) = pκ  p ≤ +}{Δ ⊢ X : κ}  \frac{Δ, X:pκ ⊢ F : κ′}{Δ ⊢ λXF : κ →^{p} κ′}

\frac{Δ ⊢ F : κ →^{p} κ′  p^{−1}Δ ⊢ G : κ}{Δ ⊢ F G : κ′}  \frac{Δ ⊢ F : κ  κ ≤ κ′}{Δ ⊢ F : κ′}

0 : ord_{u}
s : ord_{u} →^{+} ord_{g}
∞ : ord_{g}

→ : ∗_{u} →^{−} ∗_{u} →^{+} ∗_{g}
× : ∗_{u} →^{+} ∗_{u} →^{+} ∗_{g}
+ : ∗_{u} →^{+} ∗_{u} →^{+} ∗_{g}
1 : ∗_{g}

∀_{κ} : (κ →^{∘} ∗_{b}) →^{+} ∗_{b}
μ : ord_{b} →^{+} (∗_{u} →^{+} ∗_{b}) →^{+} ∗_{b}
ν : ord_{u} →^{−} (∗_{g} →^{+} ∗_{g}) →^{+} ∗_{g}

These kindings express, for instance, that successor ordinals s a and the closure ordinal ∞ are “guarded” (i.e., non-zero), each of the proper constructions →, ×, +, and 1 produces guarded types, a universal type ∀_{κ}λXA is guarded if its body A is. Interesting is the kinding of inductive types: μ^{a}F is guarded if a is non-zero and F X is guarded even for unguarded X. For example, μ^{0}F and μ^{a}λXX are always unguarded, μ^{s a}λX. 1 + X is always guarded. Finally, coinductive types ν^{a}F are always guarded, but they are only well-kinded if F maps guarded types to guarded types. Hence, the type ν^{∞}λXX, which contains only the inhabitant fix_{0}^{ν}λxx, is allowed, but ν^{a}λX.μ^{∞}λY Y is prohibited, and so is ν^{a}λX. μ^{0}F.

Type equality and subtyping. The judgement Δ ⊢ F = F′ : κ is the least congruence over the following axioms [1], including a subsumption rule:

\frac{Δ, X:pκ ⊢ F : κ′ p^{−1}Δ ⊢ G : κ}{Δ ⊢ (λXF) G = [G/X]F : κ′} \frac{Δ ⊢ F : pκ → κ′}{Δ ⊢ λX. F X = F : pκ → κ′} X ∉ FV(F)

\frac{Δ ⊢ F : ⊤κ → κ′  Δ ⊢ G : κ  Δ ⊢ G′ : κ}{Δ ⊢ F G = F G′ : κ′}

\overline{Δ ⊢ s ∞ = ∞ : ord_{g}}  \frac{Δ ⊢ a : ord_{u}  b ∈ \{u, g\}}{Δ ⊢ μ^{sa} = λF. F (μ^{a} F) : (∗_{u} →^{+} ∗_{b}) →^{+} ∗_{b}}

\frac{Δ ⊢ a : ord_{u}}{Δ ⊢ ν^{sa} = λF. F (ν^{a} F) : (∗_{g} →^{+} ∗_{g}) →^{+} ∗_{g}}

Subtyping Δ ⊢ F ≤ F′ : κ is induced by axioms expressing relations between ordinals and equipped with congruence rules that respect polarities.

\frac{Δ ⊢ a : ord_{u}}{Δ ⊢ 0 ≤ a : ord_{u}}  \frac{Δ ⊢ a : ord_{b}}{Δ ⊢ a ≤ s a : ord_{b}}  \frac{Δ ⊢ a : ord_{b}}{Δ ⊢ a ≤ ∞ : ord_{b}}

\frac{Δ ⊢ F ≤ F′ : κ →^{p} κ′ p^{−1}Δ ⊢ G : κ}{Δ ⊢ F G ≤ F′ G : κ′}

\frac{Δ ⊢ F : κ →^{+} κ′  Δ ⊢ G ≤ G′ : κ}{Δ ⊢ F G ≤ F G′ : κ′}  \frac{Δ ⊢ F : κ →^{−} κ′  Δ ⊢ G′ ≤ G : κ}{Δ ⊢ F G ≤ F G′ : κ′}

Additionally, we have a congruence rule for λ-abstraction and rules for reflexivity, transitivity, antisymmetry, and subsumption. Typically, we will use subtyping to derive μ^{a}F ≤ μ^{s a}F ≤ μ^{∞}F and ν^{∞}F ≤ ν^{s a}F ≤ ν^{a}F.

Kind interpretation. Kinds are interpreted as expected: [[∗_{u}]] = SAT_{u}, [[∗_{g}]] = SAT_{g}, [[ord_{u}]] = {α | 0 ≤ α ≤ ∞}, [[ord_{g}]] = {α | 0 < α ≤ ∞}, and [[κ →^{p} κ′]] is the space of p-variant operators from [[κ]] to [[κ′]]. For base kinds κ_{0} let A ⊑_{κ0} A′ hold iff A ⊆ A′. For higher kinds, let F ⊑_{κ→^{p}κ′} F′ iff F(G) ⊑_{κ′} F′(G) for all G ∈ [[κ]]. With these definitions, we can set

[[κ →^{p} κ′]] = {F ∈ [[κ]] → [[κ′]] | F(G) ⊑ F(G′) for all G ⊑^{p} G′ ∈ [[κ]]}.

Herein, ⊑^{+} denotes ⊑, ⊑^{−} denotes ⊒, ⊑^{∘} denotes equality, and G ⊑^{⊤} G′ always holds.

Lemma 6 (Soundness of subkinding). If κ ≤ κ′ then [[κ]] ⊆ [[κ′]].

Type interpretation. We interpret the type constants C as follows:

\begin{aligned}[[0]] & = & 0 \\ [[s]](∞) & = & ∞ \\ [[s]](α < ∞) & = & α + 1 \\ [[∞]] & = & ∞ \end{aligned} \begin{aligned}[[∀_{κ}]](F) & = & ⋂_{G∈[[κ]]} F(G) \\ [[C]] & = & C & for C ∈ \{→, ×, +, 1, μ, ν\} \end{aligned}

This interpretation can be lifted to an interpretation [[F]]_{θ} of well-kinded constructors F. We let θ ⊑ θ′ ∈ [[Δ]] if θ(X) ⊑^{p} θ′(X) ∈ [[κ]] for all (X:pκ) ∈ Δ.

Theorem 3 (Soundness of kinding, equality, and subtyping). Let θ ⊑ θ′ ∈ [[Δ]].

1. If Δ ⊢ F : κ then [[F]]_{θ} ⊑ [[F]]_{θ′} ∈ [[κ]].

2. If Δ ⊢ F = F′ : κ then [[F]]_{θ} ⊑ [[F′]]_{θ′} ∈ [[κ]].

3. If Δ ⊢ F ≤ F′ : κ then [[F]]_{θ} ⊑ [[F′]]_{θ′} ∈ [[κ]].

Typing. The rules for λ-abstraction, application, basic constants c remain in place. The type conversion rule is replaced by a subsumption rule, and the generalization and instantiation rules for universal types are now higher-kinded.

\frac{Γ ⊢ Γ (x) : ∗_{u}}{Γ ⊢ x : Γ (x)}  \frac{Γ ⊢ t : A  Γ ⊢ A ≤ B : ∗_{u}}{Γ ⊢ t : B}

\frac{Γ, X:κ ⊢ t : F X}{Γ ⊢ t : ∀_{κ}F} X ∉ FV(F)  \frac{Γ ⊢ t : ∀_{κ}F  Γ ⊢ G : κ}{Γ ⊢ t : F G}

\frac{Γ ⊢ F : ∗_{u} →^{+} ∗_{u}  Γ ⊢ G : ord_{u} →^{∘} ∗_{u}  Γ ⊢ a : ord_{u}}{Γ ⊢ fix^{μ} : (∀ı:ord_{u}. (μ^{ı}F → G ı) → μ^{s ı}F → G(s ı)) → μ^{a}F → G a} adm^{μ}

\frac{Γ ⊢ F : ∗_{g} →^{+} ∗_{g}  Γ ⊢ G_{i} : ord_{u} →^{∘} ∗_{g} for i = 1..n  Γ ⊢ a : ord_{u}}{Γ ⊢ fix_{n}^{ν} : (∀ı:ord_{u}. (G_{1..n} ı → ν^{ı}F) → G_{1..n} (s ı) → ν^{s ı}F) → G_{1..n} a → ν^{a}F} adm^{ν}

In the recursion rule, the side condition adm^{μ} needs to ensure that the type λı. μ^{ı}F → G ı is continuous in the sense of Lemma 3. Systematic criteria have been developed based on a saturated-set semantics in the context of iso-(co)in-ductive types [2], and these criteria are directly applicable for the equi-setting described in this article. Due to space restrictions, we only give a sound approximation here: There must be an n ≥ 0, Γ ⊢ F_{i} : ∗_{u} →^{+} ∗_{u} for i = 1..n and

Γ ⊢ B : ord_{u} →^{+} ∗_{u} such that Γ ⊢ G ı = μ^{ı}F_{1} → ⋯ → μ^{ı}F_{n} → B ı : ∗_{u}.

For the criterion adm^{ν} we give the following sound approximation: For each j = 1..n, either Γ ⊢ G_{j} : ord_{u} →^{−} ∗_{u}, or there exists Γ ⊢ F_{j} : ∗_{u} →^{+} ∗_{u} such that Γ ⊢ G_{j} ı = μ^{ı}F_{j} : ∗_{u}.

Theorem 4 (Soundness of typing). If Γ ⊢ t : A and θ ∈ [[Γ]] then tθ ∈ [[A]]_{θ}.

Proof. By induction on the typing derivation. The connection of the typing rules for recursion and corecursion to lemmata 3 and 4 is now immediate.

Corollary 2 (Strong normalization and consistency). Each typable term is strongly normalizing. Each closed well-typed term weak-head reduces to a value. No closed term inhabits ∀XX.

Example: Composition of Stream Processors

The sized type system encompasses a number of recursion schemes: primitive recursion, Mendler (co)recursion, course-of-value recursion, and indirect recursion (where the recursive arguments are obtained via another function, like the filtering function in case of quicksort). In the following, we implement composition comp of stream processors such that eat (comp t_{1} t_{2}) = eat t_{2} ∘ eat t_{1}. There are two possible implementations for the case that t_{1} wants to read an element and t_{2} wants to output one. We give the latter priority and arrive at the following Haskell code:

    comp :: SP a b -> SP b c -> SP a c
    comp  t1      (put c t2) = put c (comp t1 t2)
    comp (put b t1) (get f2) = comp t1 (f2 b)
    comp (get f1)        t2  = get (\ a -> comp (f1 a) t2)

We express SP through sized types and define two useful approximations of this type.

SP A B := ν^{∞}λX. μ^{∞}λY. B × X + (A → Y)
SP^{ı} A B := ν^{ı}λX. μ^{∞}λY. B × X + (A → Y)
SP^{s ı} A B = B × SP^{ı} A B + (A → SP^{s ı} A B)
put  : B × SP^{ı} A B → SP^{s ı} A B
get  : (A → SP^{s ı} A B) → SP^{s ı} A B
SP_{ȷ} A B := μ^{ȷ}λY. B × SP A B + (A → Y)
SP_{s ȷ} A B = B × SP A B + (A → SP_{ȷ} A B)
get  : (A → SP_{ȷ} A B) → SP_{s ȷ} A B
put  : B × SP_{∞} A B → SP_{s ȷ} A B

We will use the derived types of the constructors put and get below. Note the asymmetry between SP^{ı} and SP_{ȷ}, which shows in the last type of put.

In our analysis, comp t_{1} t_{2} is defined by corecursion into SPA C using a lexicographic recursion on (t_{2}, t_{1}). It is conveniently coded with a generalized recursor fix_{n}^{μ}, which recurses on the n + 1st argument and is definable from fix^{μ} [3].

comp

: SP A B → SP B C → SP A C
:= fix_{2}^{ν}Λı. λcomp^{ν}:SP A B → SP B C → SP^{ı} A C.
fix_{1}^{μ}Λȷ. λcomp_{1}^{μ}:SP A B → SP_{ȷ} B C → SP^{s ı}A C.
fix_{0}^{μ}Λk. λcomp_{2}^{μ}:SP_{k} A B → SP_{s ȷ} B C → SP^{s ı}A C.
λt_{1} :SP_{s k} A B. λt_{2} :SP_{s ȷ} B C. match t_{2} with
put (c, t′_{2} : SP B C) ↦ put (c, comp^{ν} t_{1} t′_{2}) : SP^{s ı} A C
get (f_{2} : B → SP_{ȷ} B C) ↦ match t_{1} with
put (b, t′_{1} : SP A B)  ↦ comp_{1}^{μ} t′_{1} (f_{2} b) : SP^{s ı} A C
get (f_{1} : A → SP_{k} A B) ↦ get (λa. comp_{2}^{μ} (f_{1} a) t_{2}) : SP^{s ı} A C

In the corecursive call to comp^{ν}, the first argument is casted from SP_{s k} A B to SP_{∞} A B using subtyping of inductive types. Such a cast is not available in Mendler iteration, but could be simulated with Mendler recursion. Hence, comp is a mixed coiterative/recursive/recursive function.

5 Conclusions

We have presented a construction of saturated sets for equi-inductive and coinductive types and derived two type systems which guarantee termination of recursion and corecursion under lazy unfolding. In contrast to candidates of reducibility or biorthogonals, saturated sets are closed under unions, hence, the continuity criteria for sized iso-(co)inductive types developed in previous work [2] are directly transferable to the equi-setting.

We have given two type systems for terminating (co)recursion in the presence of equi-(co)inductive types and showed by some examples that they handle mixed inductive/coinductive types properly. The system of sized types is ready for extension to higher-kinded (co)inductive types.

Although the operational semantics of corecursive values in the equi-setting suggests a semantics using biorthogonals, we have succeeded to apply a modification of the saturated sets approach. This substantiated the conjecture Colin Riba made to me, namely, biorthogonals are only required to justify languages inspired by classical logic.

Acknowledgments. The idea how to formulate guarded saturated sets came to me during a visit to the Protheo team at LORIA, Nancy in February 2007. Thanks to Frédéric Blanqui and Colin Riba for the invitation. I am also grateful to Thorsten Altenkirch who communicated the type of stream processors to me. Thanks to the anonymous referees for their valuable feedback.

References

1. Abel, A.: Polarized subtyping for sized types. In: Grigoriev, D., Harrison, J., Hirsch, E. A., eds., Proc. of the 1st Int. Computer Science Symposium in Russia, CSR 2006, volume 3967 of Lect. Notes in Comput. Sci. Springer-Verlag (2006), 381–392

2. Abel, A.: Semi-continuous sized types and termination. In: Ésik, Z., ed., Computer Science Logic, 20th Int. Workshop, CSL 2006, 15th Annual Conf. of the EACSL, volume 4207 of Lect. Notes in Comput. Sci. Springer-Verlag (2006), 72–88

3. Abel, A.: Towards generic programming with sized types. In: Uustalu, T., ed., Proc. of the 8th Int. Conf. on Mathematics of Program Construction, MPC ’06, volume 4014 of Lect. Notes in Comput. Sci. Springer-Verlag (2006), 10–28

4. Abel, A.: Strong normalization and equi-(co)inductive types. In: Ronchi Della Rocca, S., ed., Proc. of the 8th Int. Conf. on Typed Lambda Calculi and Applications, TLCA 2007, volume 4583 of Lect. Notes in Comput. Sci. Springer-Verlag (2007), 8–22

5. Abel, A., Matthes, R., Uustalu, T.: Iteration schemes for higher-order and nested datatypes. Theor. Comput. Sci. 333 (2005) 3–66

6. Amadio, R. M., Coupet-Grimal, S.: Analysis of a guard condition in type theory (extended abstract). In: Nivat, M., ed., Proc. of the 1st Int. Conf. on Foundations of Software Science and Computation Structure, FoSSaCS’98, volume 1378 of Lect. Notes in Comput. Sci. Springer-Verlag (1998), 48–62

7. Barthe, G., Frade, M. J., Giménez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Math. Struct. in Comput. Sci. 14 (2004) 1–45

8. Barthe, G., Grégoire, B., Pastawski, F.: CICˆ : Type-based termination of recursive definitions in the Calculus of Inductive Constructions. In: Hermann, M., Voronkov, A., eds., Proc. of the 13th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006, volume 4246 of Lect. Notes in Comput. Sci. Springer-Verlag (2006), 257–271

9. Blanqui, F., Riba, C.: Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems. In: Hermann, M., Voronkov, A., eds., Proc. of the 13th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006, volume 4246 of Lect. Notes in Comput. Sci. Springer-Verlag (2006), 105–119

10. Ghani, N., Hancock, P., Pattinson, D.: Continuous functions on final coalgebras. Electr. Notes in Theor. Comp. Sci. 164 (2006) 141–155

11. Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: Proc. of the 23rd ACM Symp. on Principles of Programming Languages, POPL’96 (1996), 410–423

12. Mendler, N. P.: Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic 51 (1991) 159–172

13. Parigot, M.: Recursive programming with proofs. Theor. Comput. Sci. 94 (1992) 335–356

14. Parigot, M.: Proofs of strong normalization for second order classical natural deduction. The Journal of Symbolic Logic 62 (1997) 1461–1479

15. Raffalli, C.: Data types, infinity and equality in system AF_{2}. In: Börger, E., Gurevich, Y., Meinke, K., eds., Proc. of the 7th Wksh. on Computer Science Logic, CSL ’93, volume 832 of Lect. Notes in Comput. Sci. Springer-Verlag (1994), 280–294

16. Riba, C.: On the stability by union of reducibility candidates. In: Seidl, H., ed., Proc. of the 10th Int. Conf. on Foundations of Software Science and Computational Structures, FOSSACS 2007, volume 4423 of Lect. Notes in Comput. Sci. Springer-Verlag (2007), 317–331

17. Swierstra, W.: I/O in a dependently typed programming language (2007). Talk presented at TYPES’07.