A Calculus with Recursive Types, Record
Concatenation and Subtyping
Yaoda Zhou1 , Bruno C. d. S. Oliveira1 , and Andong Fan2
The University of Hong Kong, Hong Kong SAR, China{ydzhou, bruno}@cs.hku.hk
Zhejiang University, Hangzhou, China
afan2018@zju.edu.cn

Abstract. Calculi with subtyping, a form of record concatenation andrecursive types are useful to model objects with multiple inheritance. Surprisingly, almost no existing calculi supports the three features together,
partly because the combination of subtyping and record concatenationis already known to be troublesome. Recently, a line of work on disjoint
intersection types with a merge operator has emerged as a new approachto deal with the interaction between subtyping and record concatenation.
However, the addition of recursive types has not been studied.
In this paper we present a calculus that combines iso-recursive types withdisjoint intersection types and a merge operator. The merge operator
generalizes symmetric record concatenation, and the calculus supports
subtyping as well as recursive types. We build on recent developments on
the theory of iso-recursive subtyping using the so-called nominal unfolding rules to add iso-recursive types to a calculus with disjoint intersection
types and a merge operator. The main challenge lies in the disjointness
definition with iso-recursive subtyping. We show the type soundness ofthe calculus, decidability of subtyping, as well as the soundness and completeness of our disjointness definition. All the proofs are mechanized in
the Coq theorem prover.

1

Introduction

Record calculi with a concatenation operator have attracted the attention of researchers due to their ability to give the semantics of object-oriented languages
with multiple inheritance [19,14,15]. The foundational work by Cook and Palsberg [19], and Cardelli [14] work on the semantics of the Obliq language are primeexamples of the usefulness of untyped record calculi with record concatenation
to model the semantics of OOP with inheritance.
Unfortunately, typed calculi with record concatenation and subtyping have
proven to be quite challenging to model. An important problem, identified by
Cardelli and Mitchell [15], is that subtyping can hide static type information thatis needed to correctly model (common forms of) record concatenation. Cardelliand Mitchell illustrate the problem with a simple example:
let f2 ( r :{ x : Int }) ( s :{ y : Bool }) : { x : Int } & { y : Bool } = r , , s
in f2 ({ x =3 , y =4}) ({ y = true , x = false })2Zhou et. al.

Here f2 is a function that takes two records (r and s) as arguments, and returns
a new record that concatenates the two records (r ,, s). For the return typeof f2 we use record type concatenation (here denoted as R & S). Because of
subtyping it is possible to invoke f2 with records that have more fields than thefields expected by the static types of the arguments of f2. For instance, while thestatic type of the first argument of f2 is {x : Int}, the record that is actuallyprovided at the application ({x = 3, y = 4}) also has an extra field y.
The program above is fine from a typing point of view, but what should theprogram evaluate to? There are a few common options for the semantics of record
concatenation. Record concatenation can be symmetric, only allowing the concatenation of records without conflicts; or it can be asymmetric, implementing
an overriding semantics where, in case of conflicts, fields on the left (or the right)
record are given preference. Choosing a naive form of asymmetric concatenation
does not work. For instance, with left-biased concatenation, the example above
would evaluate to {x = 3, y = 4}, which has the wrong type! Therefore, Cardelliand Mitchell [15] state that:
we should now feel compelled to define R & S only when R and S are
disjoint: that is when any field present in an element of R is absent
from every element of S, and vice versa.
hinting for an approach with symmetric concatenation, based on disjointness.
But a naive symmetric concatenation operation would result in a record {x =3, y = 4, y = true, x = false} with conflicts, which should not be allowed!
Thus, such a naive form of symmetric concatenation does not work either.
Recent work on calculi with disjoint intersection types [33] and a merge operator offers a solution to the Cardelli and Mitchell’s problem for concatenation.
For instance, the λi calculus [33] adopts disjointness and restricts subsumption
to address the challenges of symmetric concatenation/merge. Most importantly,
λi has a type-directed semantics to ensure proper information hiding and thepreservation of the expected modular type invariants. The application of the
f2 function in λi results in {x = 3, y = true}, which has no conflicts and isof the right type. Types are used at runtime to ensure that fields hidden by
subtyping are dropped from the record. This is enforced, for example, duringbeta-reduction, which uses the type of the argument to filter any hidden fields/values from records/merges. Thus, before substitution, the first argument of f2,
for instance, is first filtered using the type {x : Int}. The actual record that is
substituted in the body of f2 is {x = 3} (and not {x = 3, y = 4}).
An important limitation of existing calculi with disjoint intersection types isthat they lack recursive types. For typed model of objects, supporting recursive
types is important, since many object encodings require recursive types [10].
Without recursive types binary methods [9] and other types of methods, thatrefer to the current object type cannot be easily modelled. For example, it is hardto support an equality method in an object. In addition, recursive structures,such as lists or trees, require recursive types as well.
This paper studies subtyping relations combining iso-recursive subtyping
with disjoint intersection types and a merge operator. Our calculus λµi , extends

A Calculus with Recursive Types, Record Concatenation and Subtyping

3

λi with recursive types. With λµi we can use a standard encoding of objects
using recursive types [10,11,19,18] in λµi to model objects with recursive types.
For instance, we can define an interface for arithmetic expressions Exp using arecursive type:
Exp := µ Exp. {eval : nat, dbl : Exp, eq : Exp → bool}
In Exp there are 3 methods: an evaluation method that returns the value of evaluating the expression; a dbl method that doubles all the natural numbers in (theAST of) an expression; and an equality method that compares the expression
with another expression. In λi it is only possible to express the type of eval.
However, in λµi we can also express dbl and eq. Importantly, in λµi the record
type {eval : nat, dbl : Exp, eq : Exp → bool} is syntactic sugar for intersectionsof single field records [40,22]. In other words, to define the type Exp we needboth intersection types and recursive types.
To add iso-recursive subtyping to λµi , we employ a recent formulation of
iso-recursive subtyping based on the so-called nominal unfolding rules [47]. The
nominal unfolding rules have equivalent expressive power to the iso-recursive
Amber rules [12], but they are easier to work with formally. We prove various
important properties for λµi , including transitivity of algorithmic subtyping, decidability as well as the unfolding lemma. A key technical challenge is how todefine disjointness for iso-recursive types, which turns out to be non-trivial. By
employing the notion of a lower common supertype, we show that it is possible
to obtain a sound and complete formulation of algorithmic disjointness. All the
calculi and lemmas presented in this paper have been mechanically formalized
in the Coq theorem prover [42]. In summary, the contributions of this paper are:
– Iso-recursive subtyping with intersection types: We show the applicability of nominal unfoldings to a subtyping relation that includes intersection
types. The subtyping relation is transitive, decidable and supports the unfolding lemma.
– The λµi calculus, which adds iso-recursive types to an existing calculus
with record types, disjoint intersection types and a merge/concatenation
operator.
– Algorithmic disjointness for iso-recursive types. The algorithmic formulation of disjointness for iso-recursive types is non-trivial. We introduce anapproach based on lower common supertypes, enabling a sound and complete
algorithm for disjointness.
– Mechanical formalization: Finally, we provide a mechanical formalizationand proofs for all the calculi and proofs in the Coq theorem prover [42]. The
proofs are available in the supplementary material of this submission [46].

2

Overview

2.1

Background: Disjoint Intersection Types

λi and other calculi with disjoint intersection types [33,2,6] have been shown
to provide flexible forms of dynamic multiple inheritance [5,45]. Moreover, they

4

Zhou et. al.

enable a highly modular and compositional programming style that addresses
the Expression Problem [43] naturally. For space reasons, here we only illustratebriefly the ability of such calculi to model first-class traits and a very dynamic
form of inheritance [5]:addId ( super : Trait [ Person ] , idNumber : Int ) : Trait [ Student ]=trait inherits super = > { def id : Int = idNumber }In this code, written in the SEDEL language [5], there are two noteworthy points.
Firstly, unlike statically typed mainstream OOP languages, traits (which aresimilar to OOP classes) are first class. They can be passed as arguments (suchas super), or returned as a result as above. Secondly, the code uses a highly
dynamic form of inheritance. The trait that is inherited (super) is a parameterof the function. In contrast, in languages like Java, for class A extends B, theclass B must be statically known. We refer the interested reader to the work by[5,45] for a much more extensive discussion on the applications of calculi withdisjoint intersection types, as well as how to encode source language features,such as first-class traits.
2.2

λµi : Adding recursive types to λi

An important limitation of existing calculi with disjoint intersection types isthat they lack recursive types, preventing binary methods [9] and other types ofmethods. As we have discussed in Section 1, without recursive types we cannot
write object interfaces such as:
Exp := µ Exp. {eval : nat, dbl : Exp, eq : Exp → bool}where some method signatures refer to the type being defined. In λµi we add
recursive types, therefore it becomes possible to define the object interface Exp.
Using a standard object encoding based on records and recursive types [18,10],
we can then model objects. To implement Exp we first need a few auxiliary
functions (eval0 : Exp → nat, dbl0 : Exp → Exp and eq0 : Exp → Exp → bool) that
unfold the recursive type1 . Then we define two recursive functions lit : nat → Exp
and add : Exp → Exp → Exp:
eval0 e= (unfold [Exp] e).eval
dbl0 e= (unfold [Exp] e).dbl
eq0 e1 e2 = (unfold [Exp] e1 ).eq e2
lit n= fold [Exp]{eval = n, dbl = lit(n ∗ 2),
eq = λe0 . (eval0 e0 == n) : Exp → bool}
add e1 e2 = fold [Exp]{eval = eval0 e1 + eval0 e2 , dbl = add (dbl0 e1 ) (dbl0 e2 ),
eq = λe0 . (eval0 e0 == eval0 e1 + eval0 e2 ) : Exp → bool}
In this example the functions lit and add act as encodings of classes or traits. The
function lit is basic: it stores the literal, a double function and equality functions.
1

We assume the presence of recursive functions, and that records are lazy in theexample.

A Calculus with Recursive Types, Record Concatenation and Subtyping

5

In add, operations such as eval0 have to be called for subexpressions. To check if
2 ∗ 7 = 2 ∗ (3 + 4), we can define e1 : Exp = lit 7 and e2 : Exp = add (lit 3) (lit 4).
Then, we check if eq0 (dbl0 e1 ) (dbl0 e2 ) is satisfied.
2.3

Disjointness for Recursive Types

The disjointness restriction is an essential feature in calculi with disjoint intersection types. Such restriction ensures that certain merges of values, that could
lead to ambiguity, are forbidden. For instance, in the example above merges areused to encode records. A record {x = 1, y = true} is encoded as the merge of
two single field records {x = 1}, , {y = true}. Here the operator , , is the merge
operator [40,22], which can be viewed as a generalization of record concatenation. Ambiguity can arise with the merge operator if the two values in the merge
overlap. For instance, with records, we would like to forbid r = {x = 1, x = 2} (arecord with two fields with the same name and type), since r.x would be ambiguous. With the merge operator we can merge not only records, but also arbitraryvalues. Thus, we need to forbid merges such as 1, , 2 which provides two valuesof type Int. The disjointness restriction is employed when type-checking merges
to ensure that the types being merged do not overlap. A standard specificationof disjointness [33,29] is:Definition 1 (Specification of disjointness). Γ ` A ∗s B ≡ ∀C, (Γ ` A ≤C ∧ Γ ` B ≤ C) ⇒eCd
The intuition is that two types are disjoint when all their supertypes are (isomorphic to) >. The notation e · d represents toplike types, which are both supertypes and subtypes of >. In essence ambiguity arises from upcasts on values.
For instance if we cast 1, , 2 under type Int there can be two possible results.
Disjointness prevents merges with values having common supertypes (with the
exception of >). Therefore, when such disjoint merges are upcast we can ensurethat only one value will be extracted for any given (non toplike) type.
One of the challenges in the design of λµi is to find an algorithmic rule tocheck whether two recursive types are disjoint and prove that it is completewith respect to the specification. As part of the completeness proof we must
be able to find common supertypes of two types, but this is non-trivial for recursive types due to contravariance. For example, assume that we have tworecursive types µα. ((nat → α) → nat) and µα. ((> → α) → nat), thenµα. ((nat → α)&(> → α) → nat) is not a valid common supertype because
α is contravariant. In contrast, for covariant recursive types and non-recursive
types, finding a common supertype is simpler. For instance, for the recursive
types µα. (String → α) and µα. (nat → α), the intersection of the two inputs types of the function in the recursive type gives us a common supertypeµα. (String&nat → α).
In Section 4, we will show that the disjoint rules for recursive types are quite
simple: we only need to check if their one-time finite unfoldings are disjoint or
not. Furthermore, we can address the challenge of finding supertypes using a

6Zhou et. al.

lower common supertype definition, which gives a common supertype even forcontravariant recursive types. This plays a crucial role in the completeness proof
for disjointness.

3

Static Semantics of λµiThis section presents the static semantics of λµi , covering syntax, subtyping,disjointness and typing rules. The main novelty over λi is the addition of isorecursive types, which requires novel proof techniques to deal with disjointness.
Our subtyping relation supports intersection types and iso-recursive types using
the nominal unfolding rule [47]. Among others, we prove transitivity of subtyping, the unfolding lemma and decidability of subtyping. We note that thissubtyping relation is quite general and, while it is used by our specific application in Section 4, it can be easily adapted to many other calculi with recursive
types and intersection types.
3.1

Syntax and Subtyping

Syntax The syntax of our calculus is:
TypesA, B ::= nat | > | ⊥ | A1 → A2 | {α : A} | α | µα. A | A1 &A2Expressions
e ::= i | > | x | λx. e : A → B | e1 e2 | fix x : A. e | e : A| unfold [A] e | fold [A] e | {α = e} | e1 , , e2 | e.α
Valuesv ::= i | > | λx .e : A → B | fold [A] v | v1 , , v2 | {α = v}Contexts
Γ ::= · | Γ, α | Γ, x : A
Modes⇔ ::= ⇐ | ⇒Meta-variables A, B range over types. Types are mostly standard and consist of:natural numbers (nat), the top type (>), the bottom type (⊥), function types(A → B), type variables (α), and recursive types (µα. A). The most interesting
feature is the presence of labelled types {α : A}. Labelled types can be viewed asa simple form of nominal types. They are essentially a pair that contains a name(or type variable) α and a type. We use labelled types in two different ways: 1)
we use them with the nominal unfolding rules for iso-recursive subtyping; and2) we also use them to model records and records types in combination withintersection types and the merge operator.
Expressions, which are denoted as e, include: a top value (>), lambda expressions (λx. e : A → B) and fixpoints (fix x : A. e). Note that for lambda
expressions, we annotate both input and output types, since the output types
are necessary in a Type-Directed Operational Semantics (TDOS) during reduction, which will be described in Section 4.
Values include a canonical top value (>), lambda expressions (λx.e : A → B),
merges of values (v1 , , v2 ) and record values ({α = v}). For proving type-safety,
the contexts also store the types of variables used in the program. We employ
bi-directional type checking in the system, thus ⇐/⇒ represent the checking
mode and synthesis mode, respectively.

A Calculus with Recursive Types, Record Concatenation and Subtyping`Γ7(Well-Formed Environment)
wfe-sub`Γ
fresh αwfe-nil`·

wfe-typ`Γfresh x` Γ, αΓ `A` Γ, x : AΓ `A(Well-Formed Type)

wft-Nat`Γ

wft-Top`Γ

wft-Bot`Γ

wft-varα∈Γ

wft-arrΓ `AΓ `BΓ ` nat

Γ `>

Γ `⊥

Γ `α

Γ `A→B

wft-rcd
Γ `A

wft-recΓ, α ` A

wft-andΓ `AΓ `BΓ ` {α : A}Γ ` µα. AΓ ` A&B

Fig. 1: Well-formedness.

The syntactic sugar for record types and records is also shown below, illustrates the standard encoding [22,40] in terms of intersection types, labelled types
and merges.
{α1 : A1 , . . . , αn : An } ≡ {α1 : A1 } & . . . & {αn : An }{α1 = e1 , . . . , αn = en } ≡ {α1 = e1 } , , . . . , , {αn = en }Well-Formedness The definition of well-formed types is mostly standard, as
Figure 1 shows. An environment is well-formed if all the variables are distinct.
Subtyping Figure 2 shows the subtyping relation. Rule S-bot states that any
well-formed type A is a supertype of the ⊥ type. Rule S-fvar is a standard rule
for type variables: variable α is a subtype of itself. The rule for function types(rule S-arrow) and intersection types are standard. Rule S-rcd states that alabelled type is a subtype of another labelled type if the two types are labelledwith the same name and A ≤ B.
Rule S-rec, the nominal unfolding rule, is the most interesting one. In thisrule, the body of the recursive type is unfolded twice. However, for the innermost
unfolding, the type that we substitute is not the recursive type. Instead, we use
a labelled type, where the label is a fresh name that serves as a unique identifier
for the recursive types being compared. The label is associated to the bodies
of both recursive types. In other words, we substitute the recursive variable by
the labelled type in the recursive type body A: [α 7→ {β : A}] A. The label isuseful to identify types that arise from recursive unfolding substitutions and to
give distinct identities to recursive types. We should note that Zhou et al. [47]present the rule in a slightly different way, by reusing the recursive type variable
as a label:

8Zhou et. al.

eAd(Toplike Type)

top-basee>d

top-andeAd
eB d

top-arrow
eB d
Γ `A

top-rec
eAd

top-rcd
eAd

eA&B deA → B deµα. Ade{α : A}d

Γ `A≤B(Subtyping)

S-nat
`Γ

S-top
`Γ

Γ ` nat ≤ natΓ `A≤BS-arrowΓ ` B1 ≤ A1

S-bot
`Γ

eB d

Γ `⊥≤AΓ ` A2 ≤ B2

S-andRΓ ` A1Γ `α≤αΓ ` {α : A} ≤ {α : B }S-andΓ ` A ≤ B1

Γ ` A1 → A2 ≤ B1 → B2
S-fvar
`Γ
α∈Γ

S-rcd
Γ `A≤BΓ `A

Γ ` A ≤ B2

Γ ` A ≤ B1 &B2Γ ` A2 ≤ B

S-andLΓ ` A2

Γ ` A1 &A2 ≤ B

S-rec
Γ, α ` [α 7→ {β : A}] A ≤ [α 7→ {β : B }] BΓ ` A1 ≤ B

Γ ` A1 &A2 ≤ B
fresh βΓ ` µα. A ≤ µα. B

Fig. 2: Subtyping rules.

S-oldrecΓ, α ` [α 7→ {α : A}] A ≤ [α 7→ {α : B }] BΓ ` µα. A ≤ µα. B

The two presentations are equivalent, but the original presentation implicitly
assumes that bound variables and free variables are distinct. Thus, the α thatis bound by the recursive type µα. A and the α used in the label should beconsidered distinct (and the α used in the label should be distinct from otherfree variables as well). To avoid confusion we make such implicit assumptions
explicit in the rule S-Rec here.
The basic intuition about the nominal unfolding rules is that, in order todeal with negative occurrences of recursive type variables, such as in µα. α →nat ≤ µα. α → > we need to unfold the recursive types at least twice to detectinvalid subtyping statements. For instance, unfolding the previous example twice
leads to ((µα. α → nat) → nat) → nat ≤ ((µα. α → >) → >) → >, which is
not a valid subtyping statement. Thus, the original subtyping statement should
be rejected. The nominal unfolding rules leverage on this insight, while being
terminating since the recursive types are replaced by non-recursive types thatare in the same subtyping relation as the original types. The nominal unfoldingA Calculus with Recursive Types, Record Concatenation and Subtyping

9

rules have been shown by Zhou et al. [47] to have equivalent expressive power tothe well-known (iso-recursive) Amber rules [12]. However, the nominal unfolding
rules are easier to work with in terms of proofs, which is the reason why weemploy them here. In particular, they enable us to prove transitivity, and tohave a set of algorithmic rules (without transitivity built in). We refer interested
readers to the work by Zhou et al. for the equivalence proofs with respect to theAmber rules and the theory of the nominal unfolding rules.
A toplike type, whose definition is shown as rule S-top, is both a supertypeand a subtype of >. In calculi with disjoint intersection types, the definitionof toplike types plays an important role, since disjointness is defined in termsof toplike types. Allowing a larger set of toplike types enables more types tobe disjoint. In particular, the motivation for λi to include rule top-arrow insubtyping is to allow certain function types to be disjoint [6,28,33]. The rule toparrow itself is inspired from the well-known BCD-subtyping [4] relation, which
also states that any function type that returns a toplike type is itself toplike.
Rule top-arrow was first adopted in calculi with disjoint intersection types
by Bi et al. [6], and we follow that approach as well here. Without such rule
two function types can never be disjoint, disallowing more than one function ina merge (where all expressions must have disjoint types). Similarly, in λµi therule top-rec enables merges that can contain more than one expression with arecursive type.
Subtyping is reflexive and transitive:
Theorem 1 (Reflexivity). If ` Γ and Γ ` A then Γ ` A ≤ A.
Theorem 2 (Transitivity). If Γ ` A ≤ B and Γ ` B ≤ C then Γ ` A ≤ C.
Furthermore, we have also proved the unfolding lemma, which plays an important role in type preservation. The proof strategy is similar to the approach
used in Zhou et. al [47].
Lemma 1 (Unfolding Lemma). If Γ ` µα. A ≤ µα. B then Γ ` [α 7→µα. A] A ≤ [α 7→ µα. B] B.
3.2

Decidability

Decidability of subtyping is a significant property, which is often problematicin many subtyping relations [27,37]. Fortunately, under our new iso-recursive
subtyping rules with nominal unfoldings, decidability is easy to prove:
Theorem 3 (Decidability of Subtyping). If ` Γ , Γ ` A and Γ ` B, thenΓ ` A ≤ B is decidable.
Informally, looking at Figure 2 we can identify two potential complications inderiving an algorithm from the subtyping relation and showing its termination.
The first complication comes from the newly added intersection subtyping rules,
which makes the relation not completely syntax directed. In particular, there is

10Zhou et. al.

overlapping between all three intersection rules. However, this problem is wellknown from the literature of intersection types. A standard solution, proposedby Davies and Pfenning [21], is to only apply rule S-andL and rule S-andRfor Γ ` A1 &A2 ≤ B when B is ordinary (i.e. not an intersection type). This
removes the overlapping between rule S-and and rules S-andR and S-andL.
For the remaining overlapping between rules S-andR and S-andL backtracking is needed. The same approach can be adopted in an implementation of our
subtyping relation. The second complication is that the relation is not structurally recursive because of rule S-rec. In rule S-rec the size of the types in
the premise can actually grow. However, the key observation here is that the
number of recursive binders will reach the peak and decreases after some unfoldings. We employ the same technique by Zhou et. al [47], to prove decidability
with a nominal unfolding rule.
3.3

Disjointness

One of the core judgments of λµi is disjointness. The standard disjointness specification [33] states that two types A and B are disjoint if all common supertypesof A and B are toplike, as Definition 1 showed. In other words, A and B are disjoint if there are no non-toplike supertypes. While this definition of disjointness
is concise, it is not algorithmic. Thus, a challenge in calculi with disjoint intersection types is to find an algorithmic set of rules that is sound and complete to
the disjointness specification.
Figure 3 shows an algorithmic formulation of disjointness. Most rules are
standard and follow from previous work [33,28,7]. Toplike types are disjoint
with other types (rules dis-topL and dis-topR). Intersection types need tocheck the disjointness of every component (rules dis-andL and dis-andR). Twolabelled types are disjoint if they have distinct labels or the types of the label
are disjoint (rules dis-RcdRcd and dis-RcdRcdEq). Two different variables
are always disjoint (rule dis-VarVar). Rule dis-ArrArr states that, for two
function types, we just need to check if their output types are disjoint or not.
The most interesting one is the disjointness of recursive types. Without toplike types, it could be very simple: any two recursive types are not disjoint because µα. > is a non toplike common supertype for all recursive types. However,
the introduction of toplike types complicates the interaction between any tworecursive types, as we described in Section 2. Nevertheless, rule dis-RecRec
is surprisingly simple: two recursive types are disjoint if their bodies are disjoint. Finally, two types with different type constructors (e.g. record types andrecursive types) are disjoint (rule dis-axiom).
Disjointness soundness The soundness lemma showing that our rules satisfy the
specification is straightforward:
Lemma 2 (Soundness). If Γ ` A ∗ B then Γ ` A ∗s B.
Proof. By induction on Γ ` A ∗ B.

A Calculus with Recursive Types, Record Concatenation and SubtypingΓ `A∗B(Disjointness)

dis-topLeB d

dis-topReAdΓ `A∗BΓ `A∗B

dis-andRΓ ` A ∗ B1

11

dis-andLΓ ` A1 ∗ B

Γ ` A2 ∗ B

Γ ` A1 &A2 ∗ B

dis-VarVar
α 6= β

dis-ArrArrΓ ` A2 ∗ B2Γ `α∗βΓ ` A1 → A2 ∗ B1 → B2

dis-RcdRcd
α 6= βdis-RcdRcdEq
Γ `A∗B

dis-RecRecΓ, α ` A ∗ B

Γ ` {α : A} ∗ {β : B }Γ ` {α : A} ∗ {α : B }Γ ` µα. A ∗ µα. B

Γ ` A ∗ B2

Γ ` A ∗ B1 &B2

dis-axiomΓ ` A ∗axiom BΓ `A∗B

Fig. 3: Disjointness.

3.4

Completeness of Disjointness

The most challenging part of the formalization of λµi is to show that algorithmic disjointness is complete with respect to the specification. The difficulty isbrought by rule dis-RecRec. If two recursive types µα. A and µα. B satisfy the
specification, then for any type C, Γ ` µα. A ≤ C ∧ Γ ` µα. B ≤ C implies that
C is toplike. By rule dis-RecRec, we want to prove that any type D satisfying
Γ, α ` A ≤ D ∧ Γ, α ` B ≤ D implies that D is toplike. Clearly C and D should
be related since in one case C is the supertype of two recursive types, and in theother case D is the supertype of the bodies of the two recursive types. However,
the relation between C and D is intricate.
Lower common supertype To help to relate C and D, we define a new functiont, which is shown in Figure 4. The function t computes a lower supertype oftype A and B. A simplification that we employ in our definition is that types ofcommon supertypes in contravariant positions are all ⊥. Strictly speaking thismeans that the supertype that we find is not the lowest one in the subtyping
lattice. But in our setting this does not matter, because the disjointness of arrow
types (see rule dis-ArrArr) does not account for input types. If the input types
did matter for disjointness then we would likely need a dual definition for finding
greater common subtypes, making the definition more involved. We can provesome useful properties for t:
Lemma 3 (t is supertype). For any A and B, Γ ` A ≤ A t B and Γ ` B ≤A t B.

12

Zhou et. al.
At>
=
>
>tA
=
>
αtβ
= > (α 6= β)αtα=αA&B t C
= A&C t B&C
A t B&C= A&B t A&Cµα. A t ⊥= µα. (A t ⊥)⊥ t µα. A= µα. (⊥ t A)
{α : A} t ⊥= {α : A t ⊥}⊥ t {α : A}
= {α : ⊥ t A}
A1 → A2 t ⊥ = ⊥ → (A2 t ⊥)⊥ t A1 → A2
= ⊥ → (⊥ t A2 )µα. A t µα. B= µα. (A t B) {α : A} t {β : B} = > (α 6= β)
A1 → A2 t B1 → B2 = ⊥ → (A2 t B2 ) {α : A} t {α : B} = {α : A t B}
otherwise: ⊥ t A = A, A t ⊥ = A, A t A = A, A t B = >,Fig. 4: Lower common supertype.

Lemma 4. If Γ ` A ≤ C and Γ ` B ≤ C and A t B is toplike, then C is
toplike.
Lemma 4 is the most important one: AtB is not the least common supertypeof A and B, but if it is toplike then all supertypes of A and B are toplike. With
the previous lemmas we can prove the completeness lemma:
Lemma 5 (Completeness). For types A and B, if Γ ` A∗s B then Γ ` A∗B.
3.5

Bidirectional Typing

We use bidirectional type checking in λµi , following λi [29]. Bi-directional typechecking is helpful to eliminate a source of ambiguity (and non-determinism)that arises from an unrestricted subsumption rule in conventional type assignment systems in the presence of a concatenation/merge operator (a point which
was also noted by Cardelli and Mitchell [15]). The typing rules are shown in
Figure 5. There are two standard modes: Γ ` e ⇒ A synthesises the type A of
expression e under the context Γ , and Γ ` e ⇐ A checks if expression e has type
A under the context Γ .
Many rules are standard. There are two rules for merge expressions, which
follow from previous work [29]. Rule typing-merge employs a disjointness restriction, and only allows two expressions with disjoint types to be merged. The
disjointness restriction prevents ambiguity that could arise merging types with
common (non-toplike) supertypes. For instance, if 1, , 2 would be allowed, thenin an expression like (1, , 2) + 3 we could have two possible results: 4 and 5.
The merge of duplicated values such as 1, , 1 is not harmful, since no ambiguity
arises in this case, and such values can arise from reduction. Thus, there is also
a rule typing-mergev, which allows merging two consistent values regardlessof their types. The consistency relation is:
Definition 2 (Consistency). v1 ≈spec v2 ≡ ∀A, (v1 ,→A v10 ∧ v2 ,→A v20 ) ⇒v10 = v20

A Calculus with Recursive Types, Record Concatenation and SubtypingΓ `e⇔A

13(Typing)typing-subΓ `e ⇒ AΓ `A≤BΓ `e ⇐ B
typing-app
Γ ` e1 ⇒ A1 → A2

typing-top`Γtyping-var
`Γ
x:A∈Γ

Γ `> ⇒ >Γ `x ⇒ AΓ ` e2 ⇐ A1

Γ ` e1 e2 ⇒ A2
typing-projΓ ` e ⇒ {α : A}

typing-nat`Γtyping-annoΓ `e ⇐ AΓ ` i ⇒ natΓ `e: A ⇒ Atyping-rcd
Γ `e ⇒ AΓ ` e.α ⇒ A

Γ ` {α = e} ⇒ {α : A}

typing-abs
Γ, x : A1 ` e ⇐ A2

typing-unfoldΓ ` e ⇐ µα. A

Γ ` λx .e : A1 → A2 ⇒ A1 → A2

Γ ` unfold [µα. A] e ⇒ [α 7→ µα. A] A

typing-fix
Γ, x : A ` e ⇐ Atyping-mergeΓ ` e1 ⇒ A

Γ ` fix x : A. e ⇒ AΓ ` e2 ⇒ B

Γ `A∗BΓ ` e1 , , e2 ⇒ A&B

typing-mergev· ` v1 ⇒ A· ` v2 ⇒ B

v1 ≈spec v2

Γ ` v1 , , v2 ⇒ A&B
typing-foldΓ ` e ⇐ [α 7→ µα. A] AΓ ` µα. AΓ ` fold [µα. A] e ⇒ µα. A

Fig. 5: Typing.

In this relation, two values are consistent if for any type A casting of those twovalues under type A produces the same result. We introduce the casting relation
v1 ,→A v2 , which reduces the value v1 to v2 under the type A in Section 4.1. A
key property relating consistency and disjointness is:
Lemma 6 (Consistency of disjoint values). If ` v1 ⇒ A and ` v2 ⇒ Band ` A ∗s B then v1 ≈spec v2 .

4

Dynamic Semantics of λµi

We now introduce the Type-Directed Operational Semantics (TDOS) for λµi .
TDOS, originally proposed by Huang et al. [28,29], is a variant of small-step
operational semantics. In TDOS, type annotations are operationally relevant,since selecting values from merged values is type-directed. We show that λµi is
deterministic and type sound.

14

Zhou et. al.

v1 ,→A v2(Casting)

tred-nattred-topord A
eAd

tred-mergeL
v1 ,→A v
ord A

tred-mergeR
v2 ,→A v
ord A

i ,→nat iv ,→A A†v1 , , v2 ,→A v

v1 , , v2 ,→A v

tred-rec∼eµα. B d

· ` µα. A ≤ µα. B

fold [µα. A] v ,→µα. B fold [µα. B ] v
tred-andv ,→A v1

v ,→B v2

v ,→A&B v1 , , v2

tred-arrow∼eB2 d· ` B1 ≤ A1

· ` A2 ≤ B2

λx .e : A1 → A2 ,→B1 →B2 λx .e : A1 → B2
tred-rcd
v1 ,→A v2∼e{α : A}d{α = v1 } ,→{α:A} {α = v2 }Fig. 6: Casting.
4.1

A Type-Directed Operational Semantics for λµi

The defining feature of a TDOS is a relation called casting (originally called
typed reduction by Huang et al.). Casting plays an important role: based on
the contextual type information, values are further reduced to match the typestructure precisely. In many conventional operational semantics a value is the
final result in a program, but with TDOS further reduction can happen if thetype that is required for the value has a mismatch with the shape of the value.
For example, if we have the merge 1, ,0 c0 at type Int then casting will produce 1.
However, the same value at type Int&Char would remain unchanged (1, ,0 c0 ).
The rules for casting are shown at the Figure 6. All non-intersection types
are ordinary types. Casting v1 ,→A v2 denotes that the value v1 is reduced to v2
under the type A. From the definitions, we can see that the A is the supertypeof the principal type of v1 , and v2 is the value compatible with A. The most
special one is rule tred-top: if the type is toplike, then a value will reduce tothe corresponding top value, where the A† is defined as:(A → B)† = λx .> : A → B (µα. A)† = fold [µα. A] >{α : A}† ={α : A† }(A&B)† =A† , , B †otherwise:A† = >4.2

Reduction

The definition of reduction is shown at the Figure 7. Most rules are standard.
Casting is used in rule step-beta for adjusting the argument value to the expected type for the input of the function. Casting is also used in rule step-annov
for annotations. Rules step-fld and step-fldt are for unfold expressions.
Finally, there is also a special rule step-fldm for recursive types as well asintersection types.

A Calculus with Recursive Types, Record Concatenation and Subtyping
e1

e2(Reduction)
step-appl
e1
e10

step-beta
v1 ,→A1 v2(λx .e : A1 → A2 ) v1
step-proj
e
e0
e.α

15

([x 7→ v2 ] e) : A2

e 0 .αe1 , , e2v: Av

v1 , , e2

step-annoee0v1 , , e20e: Ae0 : Astep-fix0

fix x : A. e

step-foldee0

step-rcdee0fold [A] efold [A] e 0{α = e}step-fld
v1 ,→[α7→µα. A] A v2

v1 e20v1 e2

step-mergere2
e20

e10 , , e2

step-annov
v ,→A v 0e10 e2e1 e2

step-mergel
e1
e10

step-appr
e2
e20∼eµα. Ad

unfold [µα. A] (fold [µα. B ] v1 )v2

step-fldt
v1 ,→[α7→µα. A] A v2
unfold [µα. A] v1([x 7→ fix x : A. e] e) : A{α = e 0 }step-unfoldee0
unfold [A] e 0

unfold [A] e

step-fldm
v1 , , v2 ,→µα. A v∼eµα. Ad

unfold [µα. A] (v1 , , v2 )unfold [µα. A] v

eµα. Ad

step-projrcd

v2{α = v }.αvFig. 7: Small-step semantics.
4.3

Determinism

One of the properties of our semantics is determinism: expressions will always
reduce to the same value. Lemma 7 says that if a value can be type-checked, thenit reduces to a same value under the type A. Lemma 8 says that if an expression
can be type-checked, then it reduces to a unique expression.
Lemma 7 (Determinism of ,→). If Γ ` v ⇒ B and v ,→A v1 and v ,→A v2
then v1 = v2 .
Proof. By induction on v ,→A v1 .
Lemma 8 (Determinism of
e1 = e2 .
Proof. By induction on e
4.4). If Γ ` e ⇔ A and ee1 and ee2 thene1 .

Type safety

We prove type safety following a similar approach to the previous work [29],and by showing progress and preservation theorems. The following lemmas andtheorems show that our system is type-safe.

16

Zhou et. al.

Theorem 4 (Preservation). If ` e1 ⇔ A and e1

e2 then ` e2 ⇐ A.

Proof. By induction on ` e1 ⇔ A.
Lemma 9 (Progress of ,→). If ` v1 ⇐ A then ∃v2 , v1 ,→A v2 .
Proof. By induction on A.
Theorem 5 (Progress). If ` e1 ⇔ A then e1 is a value or ∃e2 , e1e2 .

Proof. By induction on ` e1 ⇔ A.

5

Discussion and Related Work

Throughout the paper, we have already reviewed some of the closest related
work in detail. In this section, we will discuss other related work.
Disjoint Intersection Types and Record Calculi with Concatenation. Disjoint
intersection types were originally proposed by Oliveira et al. [33]. Such calculi
have intersection types as well as a merge operator [40,22] with a disjointness
restriction to ensure the determinism of the language. Follow-up work [2,6,5]
provides more advanced features, such as disjoint polymorphism and distributive
subtyping and first-class traits, built upon the original work. With all thesefeatures together, an alternative paradigm called Compositional Programming(CP) is proposed [7,45]. CP allows for a very modular programming style where
the Expression Problem [43] can be solved naturally. A limitation of existing
calculi with disjoint intersection types is that they do not support recursive
types, which are important to encode binary methods [9] or, more generally,recursive object types. The λµi calculus addresses this limitation and shows, forthe first time, a calculus with disjoint intersection types and recursive types.
The merge operator generalizes concatenation by allowing values of any types(not just record types) to be merged. As we described in the introduction theinteraction between subtyping and record concatenation is quite tricky. Cardelliand Mitchell observed the problem [15], but did not provide a solution. Instead,they decided to use record extension and restriction operators instead of concatenation. One solution adopted by some calculi [39,38,34,26] is to distinguishbetween records that can be concatenated, and records that have subtyping. The
choice is mutually exclusive: records that can be concatenated cannot have subtyping and vice-versa. Such an approach would prevent Cardelli and Mitchell’s
f2 example in the introduction from type-checking. Calculi with disjoint intersection types, including λµi , offer a different solution by adopting a type-directedsemantics, which ensures that fields hidden by subtyping are also hidden atruntime. This allows concatenation and subtyping to be used together.
As far as we know, no full formalization of a calculus supports subtyping,record concatenation and recursive subtyping at the same time. In Cardelli’s F<:ρcalculus [13] equi-recursive subtyping is assumed to be an extension to record
subtyping and record concatenation but no proofs were provided. Palsberg andZhao’s work [34] shows supporting subtyping, record concatenation and recursive
types (but no recursive subtyping) together for type inference is NP-complete.

A Calculus with Recursive Types, Record Concatenation and Subtyping

17

Alternative Models for Typed Objects. There are alternative ways to model objects without having records and record concatenation. Perhaps the most famous
one are Abadi and Cardelli’s object calculi [1]. In their work, objects are modelled directly. No form of concatenation is provided, but the fields of objects canbe updated in object calculi. Besides, they also provide declarative type systems(with a transitivity rule built-in) to support recursive subtyping.
Another alternative approach, which has received a lot of attention recently,
are calculi with dependent object types (DOT) [41], which aims to capture theessence of Scala. Many variants of DOT include intersection types, a form ofrecursive types and subtyping. However, there are no records and record concatenation, since objects are directly modelled rather than being encoded via
records. The subtyping rules for intersection types are similar to ours. Moreover,
the rules for recursive types employed in some variants of DOT [41,44,25] aremostly structural and employ an inductive definition of subtyping. The key subtyping rules in the DOT variant by [41] are shown next:Γ, z : T1z ` T1z <: T2z
BindXΓ ` µz. T1z <: µz. T2z

Γ, z : T1z ` T1z <: T2
BindIΓ ` µz. T1z <: T2

Γ ` x : Tx
VarPackΓ ` x : µz. T zΓ ` x : µz. T z
VarUnpackΓ ` x : Tx
We adapt the notation employed by [41] for recursive types to our notation. In therules, T z denotes that variable z is free in type T . Rule BindX is in essence a onestep finite unfolding of the recursive type, leading to an inductive definition ofsubtyping. The second rule for recursive types (rule BindI) is a special case wherea recursive type µz. T1z is a subtype of another type T2 if T2 does not contain therecursive variable z. A difference between recursive types µz. T z in DOT and theones in this paper is that in DOT z is a term variable instead of a type variable. In
DOT, recursive types can be used in combination with path-dependent types [3],to denote types such as z.L, where z represents a (possibly recursive) term witha type member L. Because of this design, the typing rules that introduce andeliminate recursive types [41], are defined on variables. Unlike our formulationof subtyping, which is algorithmic, DOT’s formulation of subtyping is usuallypresented in a declarative form. Undecidability is an important problem with
DOT’s formulation of subtyping [27], and the existing decidable fragments of
DOT lack transitivity [27,31].
Semantic Subtyping with Intersection Types and Equi-Recursive Types. Semantic subtyping [24,16], provides a set-theoretic point of view for type systems.
In that approach, (equi-)recursive types and intersection types are interpreted
as subsets of the model, the subtyping relation is decidable, and some important properties, such as transitivity, are derived naturally. Although semantic
subtyping approaches have many advantages, they can be technically more involved, while the metatheory of syntactic formulations is simpler and generally
easier to extend. Damm [20] explored a type system with equi-recursive types

18

Zhou et. al.

and intersection types. His subtyping relation is quite expressive, as it supports
equi-recursive types and distributivity rules for subtyping. However, he does notfollow the conventional syntactic formulations of subtyping, such as the one inthis paper or those employed in DOT. Instead, types are encoded as regulartree expressions/set constraints. In contrast, our formulation is more conventional and supports iso-recursive types instead. Unlike our work Damm does notconsider extensible records with concatenation.
Other Languages with Recursive Types and Intersection Types. Some languages
employ recursive subtyping as well as intersection types, like Typescript [32]and Whiley [36]. Typescript has a rich type system but no formal document
provided. [8] has formalized a subset of Typescript and proved that is safe, but
unfortunately, no intersection types are supported. Whiley is an experimental
language that supports recursive types, intersection types and subtyping. However, no work formalizes all the features together, lacking either recursive types[35] or intersection types [30].

6Conclusion

Recursive types, extensible record types and intersection types are important features in many OOP languages, since object types can be modelled with recursive
records and multiple inheritance can be modelled via intersection types [17] andrecord concatenation. Our λµi calculus illustrates that the 3 features can be put
together in a single calculus and therefore can be used to provide simple encodings for objects. There are a few interesting directions for future work. One isto add polymorphism and bounded quantification to λµi , which is a significant
feature for real world languages. Another one is to investigate distributive subtyping for iso-recursive subtyping. With distributivity, we can model a form offamily polymorphism [23].

Acknowledgement
We thank the anonymous reviewers for their helpful comments. This work has
been sponsored by Hong Kong Research Grant Council projects number 17209519,
17209520 and 17209821.

References
1. Abadi, M., Cardelli, L.: A theory of objects. Springer Science & Business Media(1996)
2. Alpuim, J., Oliveira, B.C.d.S., Shi, Z.: Disjoint polymorphism. In: European Symposium on Programming. pp. 1–28. Springer (2017)
3. Amin, N., Rompf, T., Odersky, M.: Foundations of path-dependent types. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming, Systems, Languages, and Applications. OOPSLA ’14, Association for Computing Machinery (2014)

A Calculus with Recursive Types, Record Concatenation and Subtyping

19

4. Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model andthe completeness of type assignment. The journal of symbolic logic 48(4), 931–940(1983)
5. Bi, X., Oliveira, B.C.d.S.: Typed first-class traits. In: 32nd European Conference
on Object-Oriented Programming (ECOOP 2018) (2018)
6. Bi, X., Oliveira, B.C.d.S., Schrijvers, T.: The essence of nested composition.
In: 32nd European Conference on Object-Oriented Programming (ECOOP 2018)(2018)
7. Bi, X., Xie, N., Oliveira, B.C.d.S., Schrijvers, T.: Distributive disjoint polymorphism for compositional programming. In: European Symposium on Programming.
pp. 381–409. Springer, Cham (2019)
8. Bierman, G., Abadi, M., Torgersen, M.: Understanding typescript. In: European
Conference on Object-Oriented Programming. pp. 257–281. Springer (2014)
9. Bruce, K., Cardeli, L., Castagna, G., Group, T.H.O., Leavens, G.T., Pierce, B.:
On binary methods. Theory and Practice of Object Systems 1(3) (1996)
10. Bruce, K.B., Cardelli, L., Pierce, B.C.: Comparing object encodings 155(1/2),
108–133 (Nov 1999), http://www.cis.upenn.edu/~bcpierce/papers/compobj.ps
11. Cardelli, L.: A semantics of multiple inheritance. In: Semantics of Data Types(1984)
12. Cardelli, L.: Amber. In: LITP Spring School on Theoretical Computer Science. pp.
21–47. Springer (1985)
13. Cardelli, L.: Extensible records in a pure calculus of subtyping. Digital. Systems
Research Center (1992)
14. Cardelli, L.: A language with distributed scope. In: Proceedings of the 22nd
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
p. 286–297. POPL ’95 (1995)
15. Cardelli, L., Mitchell, J.C.: Operations on records. Mathematical Structures in
Computer Science 1(1), 3–48 (1991)
16. Castagna, G., Frisch, A.: A gentle introduction to semantic subtyping. In: Proceedings of the 7th ACM SIGPLAN international conference on Principles and practiceof declarative programming. pp. 198–199 (2005)
17. Compagnoni, A.B., Pierce, B.C.: Higher-order intersection types and multiple inheritance. Mathematical Structures in Computer Science (MSCS) 6(5), 469–501(1996)
18. Cook, W.R., Hill, W., Canning, P.S.: Inheritance is not subtyping. In: Proceedingsof the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages. p. 125–135. POPL ’90 (1989)
19. Cook, W.R., Palsberg, J.: A denotational semantics of inheritance and its correctness. In: Object-Oriented Programming: Systems, Languages and Applications(OOPSLA) (1989)
20. Damm, F.M.: Subtyping with union types, intersection types and recursive types.
In: International Symposium on Theoretical Aspects of Computer Software. pp.
687–706. Springer (1994)
21. Davies, R., Pfenning, F.: Intersection types and computational effects. In: International Conference on Functional Programming (ICFP) (2000)
22. Dunfield, J.: Elaborating intersection and union types. Journal of Functional Programming 24(2-3), 133–165 (2014)
23. Ernst, E.: Family polymorphism. In: European Conference on Object-Oriented
Programming (ECOOP) (2001)
24. Frisch, A., Castagna, G., Benzaken, V.: Semantic subtyping. In: Proceedings 17th
Annual IEEE Symposium on Logic in Computer Science. pp. 137–146. IEEE (2002)

20

Zhou et. al.

25. Giarrusso, P.G., Stefanesco, L., Timany, A., Birkedal, L., Krebbers, R.: Scala stepby-step: Soundness for dot with step-indexed logical relations in iris. Proc. ACM
Program. Lang. 4(ICFP) (Aug 2020)
26. Glew, N.: An efficient class and object encoding. In: Proceedings of the 15th ACM
SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, andApplications. p. 311–324. OOPSLA ’00, Association for Computing Machinery(2000)
27. Hu, J.Z., Lhoták, O.: Undecidability of dsub and its decidable fragments. Proceedings of the ACM on Programming Languages 4(POPL), 1–30 (2019)28. Huang, X., Oliveira, B.C.d.S.: A Type-Directed Operational Semantics For a
Calculus with a Merge Operator. In: 34th European Conference on ObjectOriented Programming (ECOOP 2020). vol. 166 (2020). https://doi.org/10.
4230/LIPIcs.ECOOP.2020.26
29. Huang, X., Zhao, J., Oliveira, B.C.d.S.: Taming the merge operator: a type-directed
operational semantics approach. Journal of Functional Programming (2021)
30. Jones, T., Pearce, D.J.: A mechanical soundness proof for subtyping over recursive
types. In: Proceedings of the 18th Workshop on Formal Techniques for Java-like
Programs. pp. 1–6 (2016)31. Mackay, J., Potanin, A., Aldrich, J., Groves, L.: Decidable subtyping for pathdependent types. Proceedings of the ACM on Programming Languages 4(POPL),
1–27 (2019)32. Microsoft: Typescript (2021), https://www.typescriptlang.org/
33. Oliveira, B.C.d.S., Shi, Z., Alpuim, J.: Disjoint intersection types. In: Proceedingsof the 21st ACM SIGPLAN International Conference on Functional Programming.
pp. 364–377 (2016)34. Palsberg, J., Zhao, T.: Type inference for record concatenation and subtyping. Inf.
Comput. 189(1) (Feb 2004)
35. Pearce, D.J.: Rewriting for sound and complete union, intersection and negation
types. ACM SIGPLAN Notices 52(12), 117–130 (2017)36. Pearce, D.J., Groves, L.: Whiley: a platform for research in software verification. In:
International Conference on Software Language Engineering. pp. 238–248. Springer(2013)
37. Pierce, B.C.: Bounded quantification is undecidable. Information and Computation
112(1), 131–165 (1994)
38. Pottier, F.: A 3-part type inference engine. In: European Symposium on Programming. pp. 320–335. Springer (2000)
39. Rémy, D.: A case study of typechecking with constrained types: Typing record concatenation (1995), presented at the workshop on Advances in types for computerscience at the Newton Institute, Cambridge, UK
40. Reynolds, J.C.: Preliminary design of the programming language forsythe (1988)
41. Rompf, T., Amin, N.: Type soundness for dependent object types (dot). In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented
Programming, Systems, Languages, and Applications. pp. 624–641 (2016)
42. The Coq Development Team: Coq (2019), https://coq.inria.fr
43. Wadler, P.: The expression problem (1998), discussion on the Java Genericity mailing list
44. Wang, F., Rompf, T.: Towards strong normalization for dependent object types(dot). In: 31st European Conference on Object-Oriented Programming (ECOOP2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)
45. Zhang, W., Sun, Y., Oliveira, B.C.d.S.: Compositional programming. ACM Transactions on Programming Languages and Systems (TOPLAS) pp. 1–60 (2021)

A Calculus with Recursive Types, Record Concatenation and Subtyping

21

46. Zhou, Y., Oliveira, B.C.d.S., Fan, A.: A Calculus with Recursive Types, Record
Concatenation and Subtyping (Artifact) (Aug 2022). https://doi.org/10.5281/
zenodo.7003284
47. Zhou, Y., Zhao, J., Oliveira, B.C.d.S.: Revisiting iso-recursive subtyping. ACM
Transactions on Programming Languages and Systems (TOPLAS) (2022). https://doi.org/10.1145/3549537