A Type System for Tom
Claude Kirchner
INRIA
Centre de Recherche
INRIA Bordeaux - Sud-Ouest
351, cours de la Libération,
33405 Talence Cedex France
Claude.Kirchner@inria.fr

Pierre-Etienne Moreau

Cláudia Tavares∗

INRIA & LORIA
615 rue du Jardin Botanique, CS 20101
54603 Villers-lès-Nancy Cedex France
Pierre-Etienne.Moreau@loria.fr
Claudia.Tavares@loria.fr

Extending a given language with new dedicated features is a general and quite used approach to make
the programming language more adapted to problems. Being closer to the application, this leads
to less programming flaws and easier maintenance. But of course one would still like to perform
program analysis on these kinds of extended languages, in particular type checking and inference. In
this case one has to make the typing of the extended features compatible with the ones in the starting
language.
The Tom programming language is a typical example of such a situation as it consists of an extension
of Java that adds pattern matching, more particularly associative pattern matching, and reduction
strategies.
This paper presents a type system with subtyping for Tom, that is compatible with Java’s type system,
and that performs both type checking and type inference. We propose an algorithm that checks if all
patterns of a Tom program are well-typed. In addition, we propose an algorithm based on equality
and subtyping constraints that infers types of variables occurring in a pattern. Both algorithms are
exemplified and the proposed type system is showed to be sound and complete.

1

Introduction of the problem: static typing in Tom

We consider here the Tom language, which is an extension of Java that provides rule based constructs.
In particular, any Java program is a Tom program. We call this kind of extension formal islands [4, 3]
where the ocean consists of Java code and the island of algebraic patterns. For simplicity, we consider
here only two new Tom constructs: a %match construct and a ‘ (backquote) construct.
The semantics of %match is close to the match that exists in functional programming languages, but
in an imperative context. A %match is parameterized by a list of subjects (i.e. expressions evaluated
to ground terms) and contains a list of rules. The left-hand side of the rules are patterns built upon
constructors and fresh variables, without any linearity restriction. The right-hand side is not a term, but a
Java statement that is executed when the pattern matches the subject. However, thanks to the backquote
construct (‘) a term can be easily built and returned. In a similar way to the standard switch/case
construct, patterns are evaluated from top to bottom. In contrast to the functional match, several actions
(i.e. right-hand sides) may be fired for a given subject as long as no return or break instruction is
executed. To implement a simple reduction step for each rule, it suffices to encode the left-hand side
with a pattern and consider the Java statement that returns the right-hand side.
For example, given the sort Nat and the function symbols suc and zero, addition and comparison of
Peano integers may be encoded as follows:
∗ This work was partially supported by The Capes Foundation, Ministry of Education of Brazil. Cx. postal 365, Brasília DF
70359-970, Brazil.

I. Mackie and A. Martins Moreira (Eds.): Tenth International
Workshop on Rule-Based Programming (RULE 2009)
EPTCS 21, 2010, pp. 51–63, doi:10.4204/EPTCS.21.5

A Type System for Tom

52
public Nat plus(Nat t1, Nat t2) {
%match(t1,t2) {
x,zero() -> { return ‘x; }
x,suc(y) -> { return ‘suc(plus(x,y)); }
}
}

public boolean greaterThan(Nat t1, Nat t2) {
%match(t1, t2) {
x,x
-> { return false; }
suc(x),zero() -> { return true; }
zero(),suc(y) -> { return false; }
suc(x),suc(y) -> { return ‘greaterThan(x,y); }
}
}

In this combination of an ocean language (in our case Java) and island features (in our case abstract data
types and matching), it is still an open question to perform type checking and type inference.
Since we want to allow for type inclusion at the pattern level, the first purpose of this paper is to
present an extension of the signature definition mechanism allowing for subtypes. In this context we
define Java-like types and signatures. Therefore the set of types is the union of Java types and abstract
data types (i.e. Tom types) where multiple inheritance and overloading are forbidden. For example, given
the sorts Int+ , Int− , Int and Zero, the type system accepts the declaration Int+ <: Int ∧ Int− <: Int
but refuses the declaration Zero <: Int+ ∧ Zero <: Int− . Moreover, a function symbol suc cannot be
overloaded on both sorts Int+ and Int− . In order to handle those issues, we propose an algorithm based
on unification of equality constraints [14] and simplification of subtype constraints [8, 1, 16]. It infers
the types of the variables that occur in a pattern (x and y in the previous example). Moreover, we also
propose an algorithm that checks that the patterns occurring in a Tom program are correctly typed.
Of course typing systems for algebraic terms and for rewriting has a long history. It includes the
seminal works done on OBJ, order-sorted algebras [10, 9] and Maude [6]; the works done on feature
algebras [2] or on membership constraints [11, 7]; and the works on typing rewriting in higher-order
settings like [17] or [5]. Largely inspired from these works, our contribution here focusses on the
appropriate type system for pattern-matching, possibly modulo associativity, in a Java environment.

2

Type checking

Given a signature Σv , the (simplified) abstract syntax of a Tom program is as follows:
rule
cond
term
action

::=
::=
::=
::=

cond −→ action
term1 ≺≺[s] term2 | cond1 ∧ cond2
x | f (term1 , . . . ,termn )
(term1 , . . . ,termn )

The left-hand side of a rule is a conjunction of matching conditions term1 ≺≺[s] term2 consisting of a pair
of terms and where s denotes a sort. We introduce the set F of free symbols. Terms are many-sorted
terms composed of variables x ∈ X and function symbols f ∈ F . The set of terms is written T (F , X ).
In general, an action is a Java statement, but for our purpose it is enough to consider an abstraction
consisting of terms e1 , . . . , en ∈ T (F , X ) whose instantiations are described by the conditions, and
used in the Java statement.
Example 2.1. The last rule of the greaterThan function given above can be represented by the following
rule expression:
suc(x) ≺≺[N] t1 ∧ suc(y) ≺≺[N] t2 −→ (x, y)
In a first step, we define S as a set of sorts and we consider that a context Γ is composed of a set of
pairs (variable,sort), and (function symbol,rank):
Γ ::= ∅ | Γ1 ∪ Γ2 | x : s | f : s1 , . . . , sn → s

Claude Kirchner, Pierre-Etienne Moreau, Cláudia Tavares

53

and context access is defined by the function sortOf(Γ, e) : Γ × T (F , X ) → S which returns the sort
of term e in the context Γ:
sortOf(Γ, x) = s, if x : s ∈ Γ

sortOf(Γ, f (e1, . . . , en )) = s, if f : s1 , . . . , sn → s ∈ Γ

where x ∈ X and f ∈ F .
We denote by Γ(x : s) the fact that x : s belongs to Γ. Similarly, Γ( f : s1 , . . . , sn → s) means that
f : s1 , . . . , sn → s belongs to Γ. In Fig. 1 we give a classical type checking system defined by a set of
inference rules. Starting from a context Γ and a rule expression π , we say that π is well-typed if π : wt
can be derived by applying the inference rules. wt is a special sort that corresponds to the well-typedness
of a rule or a condition cond.

Γ(x : s) ⊢ x : s

T-VAR

Γ ⊢ e1 : s1
...
Γ ⊢ en : sn
T-F UN
Γ( f : s1 , . . . , sn → s) ⊢ f (e1 , . . . , en ) : s

Γ ⊢ e1 : s
Γ ⊢ e2 : s
T-M ATCH
Γ ⊢ (e1 ≺≺[s] e2 ) : wt

Γ ⊢ (cond1 ) : wt
...
Γ ⊢ (condn ) : wt
T-C ONJ
Γ ⊢ (cond1 ∧ . . . ∧ condn ) : wt

Γ ⊢ (cond) : wt
Γ ⊢ e1 : s1
...
Γ ⊢ en : sn
T-RULE
Γ ⊢ (cond −→ (e1 , . . . , en )) : wt
if sortOf(Γ, ei ) = si , for i ∈ [1, n]

Figure 1: Simple type checking system.

2.1 Subtypes and associative-matching
In order to introduce subtypes in Tom, we refine S as the set of sorts, equipped with a partial order <:,
called subtyping. It is a binary relation on S that satisfies reflexivity, transitivity and antisymmetry.
Moreover, since we allow for some symbols to be associative, we introduce the set Fv of variadic symbols to denote them. Now, the set of terms is written T (F ∪ Fv , X ) and terms are many-sorted variadic
terms composed of variables x ∈ X and function symbols f ∈ F ∪ Fv . In the following, we often write
ℓ a variadic operator and call it a list.
We extend matching over lists to be associative. Therefore a pattern matches a subject considering
equality relation modulo flattening. Lists can be denoted by function symbols ℓ ∈ Fv or by variables
x ∈ X annotated by ∗ . Such variables, which we write x∗ , are called star variables. So we consider in
the following many-sorted variadic terms composed of variables x ∈ X , star variables x∗ (where x ∈ X )
and function symbols f ∈ F ∪ Fv . Moreover, we define that function symbols ℓ ∈ Fv with variable
domain (since they have a variable arity) of sort s1 and codomain s are written ℓ : s1 ∗ → s while star
variables x∗ are also sorted and written x∗ : s.
Since terms built from syntactic and variadic operators can have the same codomain, we cannot
distinguish one from the other only by theirs sorts. However, this is necessary to know which typing rule
applies. Moreover, an insertion of a term can be treated by two ways: given terms ℓ(e1 ), ℓ(e2 ), ℓ1 (e1 ) ∈
T (F ∪ Fv , X ) where ℓ, ℓ1 ∈ Fv , we have: 1) an insertion of a list ℓ(e1 ) into a list ℓ(e2 ) corresponds

A Type System for Tom

54

to a concatenation of these both lists resulting in ℓ(e1 , e2 ); 2) an insertion of a list ℓ1 (e1 ) into a list ℓ(e2 )
results in ℓ(ℓ1 (e1 ), e2 ). For that reason, it is important to distinguish the list from the inserted term by
its function symbol in order to define which typing rule concerned for list must be applied. For this
purpose, we introduce a notion of sorts decorated with function symbols, called types, to classify terms.
The special symbol ? is used as decoration when it is not useful to know what the function symbol is,
i.e. when the expected type is known but not the expected function symbol. This leads to a new set of
decorated sorts D which is equipped with a partial order <:s . It is a binary relation on D where sg11 <:s sg22
is equivalent to s1 <: s2 ∧ (g1 = g2 ∨ g2 =?).
As pointed out in the introduction, we assume in all that paper that the signatures considered do not
have multiple inheritance and that we do not allow function symbol overloading.
Given these notions, we refine the notion of context Γ as a set of subtyping declarations (type,type)
and pairs (variable,type), and (function symbol,rank). This is expressed by the following grammar:
∗

∗ s? | x : sg | x∗ : sℓ | f : s? , . . . , s? → s f | ℓ : (s? ) → sℓ
Γ ::= ∅ | Γ1 ∪ Γ2 | s?1 <:
s 2
n
1
1
∗ corresponds to the reflexive transitive closure of <: and context access is refined by the funcwhere <:
s
s
tion sortOf(Γ, e) : Γ × T (F ∪ Fv , X ) → D which returns the type of term e in the context Γ:

sortOf(Γ, x) = sg , if x : sg ∈ Γ
sortOf(Γ, x∗ ) = sℓ , if x∗ : sℓ ∈ Γ

sortOf(Γ, f (e1 , . . . , en )) = s f , if f : s?1 , . . . , s?n → s f ∈ Γ
∗
sortOf(Γ, ℓ(e1 , . . . , en , e)) = sℓ , if ℓ : (s?1 ) → sℓ ∈ Γ

where x ∈ X , f ∈ F , ℓ ∈ Fv , g ∈ F ∪ FV ∪ {?} and s? , s f , sg , sℓ ∈ D.
The context has at most one declaration of type or signature per term since overloading is forbidden.
This means that for e ∈ T (F ∪ Fv , X ) and sg11 , sg22 (where g1 , g2 ∈ F ∪ Fv ∪ {?} and sg11 , sg22 ∈ D) if
e : sg11 ∈ Γ and e : sg22 ∈ Γ then sg11 = sg22 . We denote by Γ(sg11 <:s sg22 ) the fact that sg11 <:s sg22 belongs to Γ.

2.2 Type checking algorithm
In Fig. 2 we give a type checking system to many-sorted variadic terms applying associative matching.
The rules are standard except for the use of decorated types. The most interesting rules are those that
apply to lists. They are three: [T-E MPTY] checks if a empty list has the same type declared in Γ; [T-E LEM]
is similar to [T-F UN] but is applied to lists; and [T-M ERGE] is applied to a concatenation of two lists of
type sℓ in Γ, resulting in a new list with same type sℓ .
The type checking algorithm reads derivations bottom-up. Since the rule [S UB] can be applied to
any kind of term, we consider a strategy where it is applied iff no other typing rule can be applied. In
practice, [S UB] will be combined with [T-VAR], [T-F UN] and [T-E LEM] and the type s?1 which appears in
the premise will be defined according to the result of function sortOf(Γ, e). The algorithm stops if it
reaches the [T-VAR] or [T-SVAR] cases, ensuring that the original expression is well-typed, or if none of
the type checking rules can be applied, raising an error.
∗

Example 2.2. Let Γ = {ℓ : (Z? ) → Zℓ , one : → None , x∗ : Zℓ , z∗ : Zℓ , y : Z? , N? <:s Z? }. Then the expression ℓ(x∗ , y, z∗ ) ≺≺[Z? ] ℓ(one()) −→ (y) is well-typed and its deduction tree is given in Fig. 3

3

Type inference

The type system presented in Section 2 needs rules to control its use in order to find the expected deduction tree of an expression. Without these rules it is possible to find more than one deduction tree for the

Claude Kirchner, Pierre-Etienne Moreau, Cláudia Tavares

T-VAR
Γ(x : sg ) ⊢ x : sg
where g ∈ F ∪ Fv ∪ {?}
Γ ⊢ e1 : s?1

Γ(x∗ : sℓ ) ⊢ x∗ : sℓ
Γ ⊢ en : s?n

...

Γ( f : s?1 , . . . , s?n → s f ) ⊢ f (e1 , . . . , en ) : s f
Γ ⊢ ℓ(e1 , . . . , en ) : sℓ

Γ ⊢ e : s?1

∗

Γ(ℓ : (s?1 ) → sℓ ) ⊢ ℓ(e1 , . . . , en , e) : sℓ
if sortOf(Γ, e) 6= sℓ and e 6= x∗
Γ ⊢ e : sg11

55

T-F UN

T-SVAR

∗

Γ(ℓ : (s?1 ) → sℓ ) ⊢ ℓ() : sℓ
Γ ⊢ ℓ(e1 , . . . , en ) : sℓ

T-E LEM

T-E MPTY
Γ ⊢ e : sℓ

∗

Γ(ℓ : (s?1 ) → sℓ ) ⊢ ℓ(e1 , . . . , en , e) : sℓ
if sortOf(Γ, e) = sℓ

T-M ERGE

where g, g1 ∈ F ∪ Fv ∪ {?}

Γ ⊢ e : sh
G EN
Γ ⊢ e : s?
if sortOf(Γ, e) = sh , where h ∈ F ∪ Fv

Γ ⊢ e1 : s?
Γ ⊢ e2 : s?
T-M ATCH
Γ ⊢ (e1 ≺≺[s? ] e2 ) : wt

Γ ⊢ (cond1 ) : wt
...
Γ ⊢ (condn ) : wt
T-C ONJ
Γ ⊢ (cond1 ∧ . . . ∧ condn) : wt

Γ(sg11

<:s

sg ) ⊢ e

: sg

S UB

g

g

Γ ⊢ (cond) : wt
Γ ⊢ e1 : s11
...
Γ ⊢ en : snn
T-RULE
Γ ⊢ (cond −→ (e1 , . . . , en )) : wt
gi
if sortOf(Γ, ei ) = si , where gi ∈ F ∪ Fv ∪ {?} for i ∈ [1, n]

Figure 2: Type checking rules.
same expression. For instance, in Example 2.2, the rule [S UB] can be applied to the leaves resulting of
application of rule [T-VAR]. The resulting tree will still be a valid deduction tree since the variables in
the leaves will have type N? instead of type Z? declared in the context and N? <:s Z? . For that reason, we
are interested in defining another type system able to infer the most general types of terms. We add type
variables in the set of types (defined up to here as a set of decorated sorts) to describe a possibly infinite
set of decorated sorts. The set of types Type (D ∪ {wt}, V ) is given by a set of decorated sorts D, a set of
type variables V and a special sort wt:
τ ::= α | sg | wt
where τ ∈ Type (D ∪ {wt}, V ), α ∈ V , g ∈ F ∪ Fv ∪ {?} and sg ∈ D.
In order to build the subtyping rule into the rules, we use a constraint set C to store all equality and
subtyping constraints. These constraints limit types that terms can have. The language C is built from
the set of types Type (D ∪ {wt}, V ) and the operators “=s ” (equality) and “<:s ” (extension to Type (D ∪
{wt}, V ) of the partial order defined in Subsection 2.1):
c ::= τ1 =s τ2 | τ1 <:s τ2
where c ∈ C , τ1 , τ2 ∈ Type (D ∪ {wt}, V ).
A substitution σ is said to satisfy an equation τ1 =s τ2 if σ τ1 = σ τ2 . Moreover, σ is said to satisfy a
subtype relation τ1 <:s τ2 if σ τ1 <:s σ τ2 .
Thus, σ is a solution for C if it satisfies all constraints in C. This is written σ |= C. The set V (C)
denotes the set of type variables in C.

A Type System for Tom

56

Γ ⊢ ℓ() : Zℓ

T-E MPTY

Γ ⊢ ℓ(x∗ ) : Zℓ

Γ ⊢ x∗ : Zℓ

T-SVAR
T-M ERGE

Γ ⊢ y : Z?

Γ ⊢ ℓ(x∗ ,y) : Zℓ

T-VAR
T-E LEM

Γ ⊢ ℓ(x∗ ,y,z∗ ) : Zℓ

Γ ⊢ z∗ : Zℓ

T-SVAR
T-M ERGE

T-G EN
Γ ⊢ ℓ(x∗ ,y,z∗ ) : Z?
··
··
··
Γ ⊢ one() : None
··
Γ ⊢ one() : N?
··
T-E MPTY
··
ℓ
Γ ⊢ ℓ() : Z
Γ ⊢ one() : Z?
··
··
Γ ⊢ ℓ(one()) : Zℓ
··
··
Γ ⊢ ℓ(one()) : Z?
Γ ⊢ (ℓ(x∗ ,y,z∗ ) ≺≺[Z? ] ℓ(one())) : wt

T-F UN
G EN
S UB
T-E LEM
T-G EN
T-M ATCH

Γ ⊢ (ℓ(x∗ ,y,z∗ ) ≺≺[Z? ] ℓ(one()) −→ (y)) : wt

Γ ⊢ y : Z?

T-VAR
T-RULE

Figure 3: Type checking example.
Constraints are calculated according to the application of rules of type inference system (see Fig. 4)
where we can read the judgment Γ ⊢ct e : τ •C as “the term e has type τ under assumptions Γ whenever
the constraints C are satisfied”. More formally, this judgment states that ∀σ  (σ |= C → σ Γ ⊢ e : σ τ ).

3.1 Type inference algorithm
In Fig. 4 we give a type inference system with constraints. In order to infer the type of a given expression π , the context Γ is initialized to: 1) subtype declarations of the form s?1 <:s s?2 where s?1 and s?2 ∈ D;
2) a pair of the form ( f : s?1 , . . . , s?n → s f ) for each syntactic operator f occurring in π where s?i , s f ∈ D for
∗
i ∈ [1, n]; 3) a pair of the form (ℓ : s?1 → sℓ ) for each variadic operator ℓ occurring in π where s?1 , sℓ ∈ D;
4) a pair of the form (x : α ) for each variable x occurring in π where α ∈ V is a fresh type variable; 5) a
pair of the form (x∗ : α ) for each star variable x∗ occurring in π where α ∈ V is a fresh type variable.
Moreover, each type variable introduced in a sub-derivation is a fresh type variable and the fresh type
variables in different sub-derivations are distinct. As in Section 2.2, we explain the rules concerning
lists: [CT-E MPTY] infers for an empty list ℓ() a type variable α with the constraint α = sℓ , sℓ given by
the rank of ℓ; [CT-E LEM] treats applications of lists to elements which are neither lists with the same
function symbol nor star variables; [CT-M ERGE] is applied to concatenate two lists of same type sℓ ; and
[CT-S TAR] is applied to concatenate a list and a star variable of the same type sℓ .
∗

Example 3.1. Let Γ = {ℓ : (Z? ) → Zℓ , one : → None , x∗ : α1 , y : α2 , z∗ : α3 , N? <:s Z? }. Then the expression ℓ(x∗ , y, z∗ ) ≺≺[α4 ] ℓ(one()) −→ (y) is well-typed and the deduction tree is given in Fig. 5.

3.2 Constraint resolution
In Fig. 6 we propose an algorithm to decide whether a given constraint set C has a solution, where g1 , g2 ∈
F ∪ Fv ∪ {?}. We denote by sg1 <:s s′g2 ∈ Γ the fact that there exists s1 , . . . , sn such that s? <: s?1 ∈ Γ,
s?1 <: s?2 ∈ Γ, . . . , s?n <: s′? ∈ Γ and (g1 = g2 or g2 =?). If the algorithm stops without failure then C is said
to be in solved form.
While solving a constraint set C we wish to make sure, after each application of a constraint resolution
rule, that the constraint set at hand is satisfiable, so as to detect errors as soon as possible. Therefore we

Claude Kirchner, Pierre-Etienne Moreau, Cláudia Tavares

Γ(x : τ ) ⊢ct x : α • {α =s τ }

CT-VAR

Γ ⊢ct e1 : α1 •C1

57

Γ(x∗ : α1 ) ⊢ct x∗ : α • {α1 =s α }
...

Γ ⊢ct en : αn •Cn

Γ( f : s?1 , . . . , s?n → s f ) ⊢ct f (e1 , . . . , en ) : α • {α =s s f }

n
S
i=1

∗

Γ(ℓ : (s?1 ) → sℓ ) ⊢ct ℓ() : α • {α =s sℓ }
Γ ⊢ct ℓ(e1 , . . . , en ) : α •C1
Γ(ℓ :

∗
(s?1 )

→

sℓ ) ⊢

ct

Γ(ℓ :

→

sℓ ) ⊢

ct

Γ(ℓ

∗
: (s?1 )

Γ ⊢ct e : α1 •C2

Γ ⊢ct e : α •C2

ℓ(e1 , . . . , en , e) : α • {α =s sℓ } ∪C1 ∪C2
if sortOf(Γ, e) = sℓ

Γ ⊢ct ℓ(e1 , . . . , en ) : α •C1

CT-F UN

CT-E MPTY

ℓ(e1 , . . . , en , e) : α • {α =s sℓ , α1 <:s s?1 } ∪C1 ∪C2
if sortOf(Γ, e) 6= sℓ and e 6= x∗

Γ ⊢ct ℓ(e1 , . . . , en ) : α •C1
∗
(s?1 )

Ci ∪ {αi <:s s?i }

CT-SVAR

CT-E LEM

CT-M ERGE

Γ ⊢ct x∗ : α •C2

→ sℓ ) ⊢ct ℓ(e1 , . . . , en , x∗ ) : α • {α =s sℓ } ∪C1 ∪C2

CT-S TAR

Γ ⊢ct e2 : α2 •C2
Γ ⊢ct e1 : α1 •C1
CT-M ATCH
Γ ⊢ct (e1 ≺≺[τ ] e2 ) : wt • {α1 <:s τ , α2 =s τ } ∪C1 ∪C2
Γ ⊢ct (cond1 ) : wt •C1

...

Γ ⊢ct (condn ) : wt •Cn

Γ ⊢ct (cond1 ∧ . . . ∧ condn ) : wt •

n
S

CT-C ONJ

Ci

i=1

Γ ⊢ct (cond) : wt •Ccond

Γ ⊢ct e1 : τ1 •C1

...

Γ ⊢ct (cond −→ (e1 , . . . , en )) : wt •Ccond

Γ ⊢ct en : τn •Cn
n
S

CT-RULE

Ci

i=1

if sortOf(Γ, ei ) = τi , for i ∈ [1, n] where τi ∈ Type (D ∪ {wt}, V )

Figure 4: Type inference rules.

must combine the rules for error detection and constraint resolution in order to keep C in solved form. The
rules for the constraint resolution algorithm are provided in Fig. 7, where g, g1 , g2 ∈ F ∪ Fv ∪ {?}. The
rules (1)-(14) are recursively applied over C. More precisely, rules (1)-(3) work as a garbage collector
removing constraints that are no more useful. Rules (4) and (5) generate σ . Rules (6) and (7) generate
more simplified constraints. Rules (8)-(12) generate σ and simplified constraints by antisymmetric and
transitive subtype closure. Rules (13) and (14) are applied when none of previous rules can be applied
generating a new σ from a constraint over a type variable that has no other constraints. The algorithm

A Type System for Tom

58

Γ ⊢ct ℓ() : α5 •C3 = {α5 =s Zℓ }

CT-E MPTY

Γ ⊢ct x∗ : α5 •C4 = {α5 =s α1 }

Γ ⊢ct ℓ(x ) : α5 •C2 = {α5 =s Z } ∪C3 ∪C4
∗

ℓ

CT-SVAR
CT-S TAR

Γ ⊢ct y : α8 •C5 = {α8 =s α2 }

Γ ⊢ct ℓ(x ,y) : α5 •C1 = {α5 =s Z , α8 <:s Z } ∪C2 ∪C5
··
··
CT-SVAR
···
Γ ⊢ct z∗ : α5 •C6 = {α5 =s α3 }
·
CT-S TAR
Γ ⊢ct ℓ(x∗ ,y,z∗ ) : α5 •Cp = {α5 =s Zℓ } ∪C1 ∪C6
ℓ

∗

?

CT-VAR
CT-E LEM

(1)

Γ ⊢ct ℓ() : α6 •C7 = {α6 =s Zℓ }

CT-E MPTY

Γ ⊢ct one() : α7 •C8 {α7 =s None }

Γ ⊢ct ℓ(one()) : α6 •Cs = {α6 =s Zℓ , α7 <:s Z? } ∪C7 ∪C8

CT-F UN
CT-E LEM

(2)

(1)
(2)
CT-M ATCH
CT-VAR
Γ ⊢ct (ℓ(x∗ ,y,z∗ ) ≺≺[α4 ] ℓ(one())) : wt •Ccond = {α5 <:s α4 , α6 =s α4 }
Γ ⊢ct y : α9 •C10 = {α9 =s α2 }
CT-RULE
∗
∗
Γ ⊢ct (ℓ(x ,y,z ) ≺≺[α4 ] ℓ(one()) −→ (y)) : wt •Cr = {α2 =s α2 } ∪Ccond ∪C10

Figure 5: Type inference example.

(1)
(2)
(3)
(4)
(5)

{sg11 <:s α , α <:s sg22 } ⊎C′
{sg11 <:s α , sg22 <:s α } ⊎C′
{α <:s sg11 , α <:s sg22 } ⊎C′
{sg11 <:s sg22 } ⊎C′
{sg11 = sg22 } ⊎C′

=⇒
=⇒
=⇒
=⇒
=⇒

f ail
f ail
f ail
f ail
f ail

if sg11 <:s sg22 ∈
/Γ
if 6 ∃s  (sg11 <:s s? ∈ Γ ∧ sg22 <:s s? ∈ Γ)
if (sg11 <:s sg22 ∈
/ Γ ∧ sg22 <:s sg11 ∈
/ Γ)
g1
g2
if s1 <:s s2 ∈
/Γ
if s1 6= s2 ∨ g1 6= g2

Figure 6: Rules for detection of errors in a constraint set C.
stops if: a rule returns C = ∅, then the algorithm returns the solution σ ; if C reaches a non-solved form,
then the algorithm for detection of errors returns f ail; or if C reaches a normal form different from the
empty set, then the algorithm returns an error. We say that the algorithm is failing if it returns either fails
or an error.
∗

Example 3.2. Let Γ = {ℓ : (Z? ) → Zℓ , one : → None , x∗ : α1 , y : α2 , z∗ : α3 , N? <:s Z? } and Ccond = {α5 =s
Zℓ , α10 =s α1 , α5 =s Zℓ , α10 =s Zℓ , α9 =s α2 , α5 =s Zℓ , α9 <:s Z? , α8 =s α3 , α5 =s Zℓ , α8 =s Zℓ , α6 =s
Zℓ , α7 =s None , α6 =s Zℓ , α7 <:s Z? , α5 <:s α4 , α6 =s α4 , α2 =s α2 } from the Example 3.1. Let σ = ∅ and
C = Ccond . The constraint resolution algorithm starts by:
1. Application of sequence of rules (4), (1) and (5) generating {α2 <:s Z? , None <:s Z? , Zℓ <:s Zℓ } ∪C
and {α5 7→ Zℓ , α10 7→ α1 , α1 7→ Zℓ , α9 7→ α2 , α8 7→ α3 , α3 7→ Zℓ , α6 7→ Zℓ , α7 7→ None , α4 7→ Zℓ } ∪
σ
2. Application of rules (1), (2) and (3) generating {α2 <:s Z? } and σ ;

Claude Kirchner, Pierre-Etienne Moreau, Cláudia Tavares

59

(1)
(2)
(3)

{τ =s τ } ⊎C′ , σ
{τ <:s τ } ⊎C′ , σ
{sg11 <:s sg22 } ⊎C′ , σ

=⇒
=⇒
=⇒

C′ , σ
C′ , σ
C′ , σ if sg11 <:s sg22 ∈ Γ

(4)
(5)

{α =s τ } ⊎C′ , σ
{τ =s α } ⊎C′ , σ

=⇒
=⇒

[α →
7 τ ]C′ , {α →
7 τ} ∪ σ
[α →
7 τ ]C′ , {α →
7 τ} ∪ σ

(6)
(7a)
(7b)

{sg11 <:s α , sg22 <:s α } ⊎C′ , σ
{α <:s sg11 , α <:s sg22 } ⊎C′ , σ
{α <:s sg11 , α <:s sg22 } ⊎C′ , σ

=⇒
=⇒
=⇒

{s? <:s α } ∪C′ , σ if ∃s  (sg11 <:s s? ∈ Γ ∧ sg22 <:s s? ∈ Γ)
{α <:s sg11 } ∪C′ , σ if (sg11 <:s sg22 ∈ Γ)
{α <:s sg22 } ∪C′ , σ if (sg22 <:s sg11 ∈ Γ)

(8)
(9)
(10)
(11)
(12)

{τ1 <:s τ2 , τ2 <:s τ1 } ⊎C′ , σ
{α1 <:s α , α <:s α2 } ⊎C′ , σ
{sg <:s α , α <:s α1 } ⊎C′ , σ
{α1 <:s α , α <:s sg } ⊎C′ , σ
{sg11 <:s α , α <:s sg22 } ⊎C′ , σ

=⇒
=⇒
=⇒
=⇒
=⇒

{τ1 =s τ2 } ∪C′ , σ
{α1 <:s α2 } ∪ [α 7→ α2 ]C′ , {α 7→ α2 } ∪ σ
{sg <:s α1 } ∪ [α 7→ α1 ]C′ , {α 7→ α1 } ∪ σ
{α1 <:s sg } ∪ [α 7→ α1 ]C′ , {α 7→ α1 } ∪ σ
[α 7→ sg22 ]C′ , {α 7→ sg22 } ∪ σ if sg11 <:s sg22 ∈ Γ

(13)
(14)

{α <:s τ } ⊎C′ , σ
{τ <:s α } ⊎C′ , σ

=⇒
=⇒

C′ , {α →
7 τ } ∪ σ if α ∈
/ V (C′ )
′
C , {α →
7 τ } ∪ σ if α ∈
/ V (C′ )

Figure 7: Constraint resolution rules in context Γ.
3. Application of rule (13) generating ∅ and {α2 7→ Z? } ∪ σ , the algorithm then stops and returns σ
providing a substitution for all type variables in the deduction tree of ℓ(x∗ , y, z∗ ) ≺≺[α4 ] ℓ(one()) −→
(y).

4

Properties

Since our type checking system and our type inference system address the same issue, we must check
two properties. First, we show that every typing judgment that can be derived from the inference rules
also follows from the checking rules (Theorem 4.2), in particular the soundness. Then we show that
a solution given by the checking rules can be extended to a solution proposed by the inference rules
(Theorem 4.4).
Definition 4.1 (Solution). Let Γ be a context and e a term.
• A solution for (Γ, e) is a pair (σ , T1 ) such that σ Γ ⊢ σ e : T1 , where T1 ∈ D ∪ {wt}.
• Assuming a well-formed sequent Γ ⊢ e : τ •C, a solution for (Γ, e, τ ,C) is a pair (σ , T2 ) such that
σ satisfies C and σ τ <:s T2 , where T2 ∈ D ∪ {wt} and τ ∈ Type (D ∪ {wt}, V ).
Theorem 4.2 (Soundness of constraint typing). Suppose that Γ ⊢ct e : τ •C is a valid sequent. If (σ , sg )
is a solution for (Γ, e, τ ,C), then it is also a solution for (Γ, e) (i.e. e is well-typed in Γ).
Proof. By induction on the given constraint typing derivation for Γ ⊢ct e : τ •C. We just detail the most
noteworthy cases of this proof.

A Type System for Tom

60
Case CT-E LEM:

τ =α
Γ ⊢ct a : α1 •C2

e = ℓ(a1 , . . . , an , a)
Γ ⊢ct ℓ(a1 , . . . , an ) : α •C1
C = C1 ∪C2 ∪ {α =s sℓ2 , α1 <:s s?1 }
∗

We are given that (σ , sg ) is a solution for (Γ(ℓ : (s?1 ) → sℓ2 ), e, α ,C), that is, σ satisfies C and σ α <:s
g
s . Since (σ , sg ) satisfies C1 and C2 , (σ , σ α ) and (σ , σ α1 ) are solutions for (Γ, ℓ(a1 , . . . , an ), α ,C1 ) and
(Γ, a, α1 ,C2 ), respectively. By the induction hypothesis, we have σ Γ ⊢ σ (ℓ(a1 , . . . , an )) : σ α and σ Γ ⊢
σ a : σ α1 . Since σ α1 <:s s?1 , by S UB we obtain σ Γ ⊢ σ a : s?1 . Since σ α = sℓ2 , by T-E LEM we obtain σ (Γ(ℓ :
∗
∗
(s?1 ) → sℓ2 )) ⊢ σ (ℓ(a1 , . . . , an , a)) : sℓ2 . By S UB we obtain σ (Γ(ℓ : (s?1 ) → sℓ2 )) ⊢ σ (ℓ(a1 , . . . , an , a)) : sg ,
as required.
Case CT-M ERGE:

e = ℓ(a1 , . . . , an , a)
Γ ⊢ct ℓ(a1 , . . . , an ) : α •C1
C = C1 ∪C2 ∪ {α =s sℓ2 }

τ =α
Γ ⊢ct a1 : α •C2
∗

We are given that (σ , sg ) is a solution for (Γ(ℓ : (s?1 ) → sℓ2 ), e, α ,C), that is, σ satisfies C and σ α <:s
g
s . Since (σ , sg ) satisfies C1 and C2 , (σ , σ α ) and (σ , σ α1 ) are solutions for (Γ, ℓ(a1 , . . . , an ), α ,C1 ) and
(Γ, a, α ,C2 ). By the induction hypothesis, we have σ Γ ⊢ σ (ℓ(a1 , . . . , an )) : σ α and σ Γ ⊢ σ a : σ α1 .
∗
Since σ α = sℓ2 , by T-M ERGE we obtain σ (Γ(ℓ : (s?1 ) → sℓ2 )) ⊢ σ (ℓ(a1 , . . . , an , a)) : sℓ2 . By S UB we obtain
∗
σ (Γ(ℓ : (s?1 ) → sℓ2 )) ⊢ σ (ℓ(a1 , . . . , an , a)) : sg , as required.
Case CT-M ATCH:

e = a1 ≺≺[τ1 ] a2
Γ ⊢ct a1 : α1 •C1
C = C1 ∪C2 ∪ {α1 <:s τ1 , α2 =s τ1 }

τ = wt
Γ ⊢ct a2 : α2 •C2

We are given that (σ , wt) is a solution for (Γ, e, wt,C), that is, σ satisfies C and σ wt <:s wt. Since
(σ , wt) satisfies C1 and C2 , (σ , σ α1 ) and (σ , σ α2 ) are solutions for (Γ, a1 , α1 ,C1 ) and (Γ, a2 , α2 ,C2 ),
respectively. By the induction hypothesis, we have σ Γ ⊢ σ a1 : σ α1 and σ Γ ⊢ σ a2 : σ α2 . Since σ α1 <:s
σ τ1 , by S UB we obtain σ Γ ⊢ σ a1 : σ τ1 . Since σ α2 = σ τ1 , by T-M ATCH we obtain σ Γ ⊢ σ (a1 ≺≺[τ1 ] a2 ) :
wt, as required.
Definition 4.3 (Normal form of typing derivation). A typing derivation is in normal form if it does not
have successive applications of rule [ S UB ].
Theorem 4.4 (Completeness of constraint typing). Suppose that π = Γ ⊢ct e : τ •C. Write V (π ) for the
set of all type variables mentioned in the last rule used to derive π and write σ \V (π ) for the substitution
that is undefined for all the variables in V (π ) and otherwise behaves like σ . If (σ , sg ) is a solution for
(Γ, e) and dom(σ )∩V (π ) = ∅, then there is some solution (σ ′ , sg ) for (Γ, e, τ ,C) such that σ ′ \V (π ) = σ .
Proof. By induction on the given constraint typing derivation in normal form, but we must take care with
fresh names of variables. We just detail the most noteworthy cases of this proof.
Case CT-E LEM:

e = ℓ(a1 , . . . , an , a)
π1 = Γ ⊢ct ℓ(a1 , . . . , an ) : α •C1
C = C1 ∪C2 ∪ {α =s sℓ2 , α1 <:s s?1 }
sortOf(Γ, a) 6= sℓ2

τ =α
π2 = Γ ⊢ct a : α1 •C2
V (π ) = {α , α1 }

Claude Kirchner, Pierre-Etienne Moreau, Cláudia Tavares

61
∗

From the assumption that (σ , sg ) is a solution for (Γ(ℓ : (s?1 ) → sℓ2 ), ℓ(a1 , . . . , an , a)) and dom(σ ) ∩
∗
V (π ) = ∅, we have σ (Γ(ℓ : (s?1 ) → sℓ2 )) ⊢ σ (ℓ(a1 , . . . , an , a)) : sg . This can be derived from: 1) T-M ERGE,
2) T-E LEM or 3) S UB. In all those cases, we must exhibit a substitution σ ′ such that: (a) σ ′ \V (π ) agrees
with σ ; (b) σ ′ α <:s sg ; (c) σ ′ satisfies C1 and C2 ; and (d) σ ′ satisfies {α =s sℓ2 , α1 <:s s?1 }. We reason by
cases as follows:
1. By T-M ERGE we assume that sg = sℓ2 and we know that σ Γ ⊢ σ (ℓ(a1 , . . . , an )) : sℓ2 and σ Γ ⊢ σ a : sℓ2 .
But since we cannot find a type sℓ3 such that sℓ3 <:s sℓ2 , σ Γ ⊢ σ a : sℓ2 cannot be derived even from
S UB. Thus T-M ERGE is not a relevant case.
2. By T-E LEM we assume that sg = sℓ2 and we know that σ Γ ⊢ σ (ℓ(a1 , . . . , an )) : sℓ2 and σ Γ ⊢ σ a : s?1 .
By the induction hypothesis, there are solutions (σ1 , sℓ2 ) for (Γ, ℓ(a1 , . . . , an ), α ,C1 ) and (σ2 , s?1 )
for (Γ, a, α1 ,C2 ), and dom(σ1 )\V (π1 ) = ∅ = dom(σ2 )\V (π2 ). Define σ ′ = {α 7→ sℓ2 , α1 7→ s?1 } ∪
σ ∪ σ1 ∪ σ2 . Conditions (a), (b), (c) and (d) are obviously satisfied. Thus, we see that (σ ′ , sg ) is a
∗
solution for (Γ(ℓ : (s?1 ) → sℓ2 ), ℓ(a1 , . . . , an , a), α ,C).
∗

3. By S UB we assume that sℓ2 <:s sg ∈ Γ and we know that σ (Γ(ℓ : (s?1 ) → sℓ2 )) ⊢ σ (ℓ(a1 , . . . , an , a)) :
sℓ2 . This must be derived from T-E LEM, similar to case (2).
Case CT-M ERGE:

e = ℓ(a1 , . . . , an , a)
π1 = Γ ⊢ct ℓ(a1 , . . . , an ) : α •C1
C = C1 ∪C2 ∪ {α =s sℓ2 }
sortOf(Γ, a) = sℓ2

τ =α
π2 = Γ ⊢ct a : α •C2
V (π ) = {α }
∗

From the assumption that (σ , sg ) is a solution for (Γ(ℓ : (s?1 ) → sℓ2 ), ℓ(a1 , . . . , an , a)) and dom(σ ) ∩
∗
V (π ) = ∅, we have σ (Γ(ℓ : (s?1 ) → sℓ2 )) ⊢ σ (ℓ(a1 , . . . , an , a)) : sg . This can be derived from: 1) T-M ERGE,
2) T-E LEM or 3) S UB. In all those cases, we must exhibit a substitution σ ′ such that: (a) σ ′ \V (π ) agrees
with σ ; (b) σ ′ α <:s sg ; (c) σ ′ satisfies C1 and C2 ; and (d) σ ′ satisfies {α =s sℓ2 }. We reason by cases as
follows:
1. By T-M ERGE we assume that sg = sℓ2 and we know that σ Γ ⊢ σ (ℓ(a1 , . . . , an )) : sℓ2 and σ Γ ⊢ σ a : sℓ2 .
By the induction hypothesis, there are solutions (σ1 , sℓ2 ) for (Γ, ℓ(a1 , . . . , an ), α ,C1 ) and (σ2 , sℓ2 ) for
(Γ, a, α ,C2 ), and dom(σ1 )\V (π1 ) = ∅ = dom(σ2 )\V (π2 ). Define σ ′ = {α 7→ sℓ2 } ∪ σ ∪ σ1 ∪ σ2 .
Conditions (a), (b), (c) and (d) are obviously satisfied. Thus, we see that (σ ′ , sg ) is a solution for
∗
(Γ(ℓ : (s?1 ) → sℓ2 ), ℓ(a1 , . . . , an , a), α ,C).
2. By T-E LEM we assume that sg = sℓ2 and we know that σ Γ ⊢ σ (ℓ(a1 , . . . , an )) : sℓ2 and σ Γ ⊢ σ a : s?1 .
But, because of the application condition of T-E LEM, we cannot find a type sℓ1 for σ a such that
sℓ1 <:s s?1 , σ Γ ⊢ σ a : s?1 cannot be derived from G EN. Likewise, since we cannot find a type sℓ3
for σ a such that sℓ3 <:s s?1 , σ Γ ⊢ σ a : s?1 cannot be derived even from S UB. Thus T-E LEM is not a
relevant case.
∗

3. By S UB we assume that sℓ2 <:s sg ∈ Γ and we know that σ (Γ(ℓ : (s?1 ) → sℓ2 )) ⊢ σ (ℓ(a1 , . . . , an , a)) :
sℓ2 . This must be derived from T-M ERGE, similar to case (1).
Case CT-M ATCH:

e = a1 ≺≺[τ1 ] a2
π1 = Γ ⊢ct a1 : α1 •C1
C = C1 ∪C2 ∪ {α1 <:s τ1 , α2 =s τ1 }

τ = wt
π2 = Γ ⊢ct a2 : α2 •C2
V (π ) = {α1 , α2 , τ1 } if τ1 ∈ V
/V
V (π ) = {α1 , α2 } if τ1 ∈

A Type System for Tom

62

From the assumption that (σ , wt) is a solution for (Γ, a1 ≺≺[τ1 ] a2 ) and dom(σ ) ∩ V (π ) = ∅, we
have σ Γ ⊢ σ (a1 ≺≺[τ1 ] a2 ) : wt. This must be derived from T-M ATCH, we know that σ Γ ⊢ σ a1 : σ τ1
and σ Γ ⊢ σ a2 : σ τ1 . By the induction hypothesis, there are solutions (σ1 , σ τ1 ) for (Γ, a1 , α1 ,C1 ) and
(σ2 , σ τ1 ) for (Γ, a2 , α2 ,C2 ). We must exhibit a substitution σ ′ such that: (a) σ ′ \V (π ) agrees with σ ; (b)
σ ′ wt <:s wt; (c) σ ′ satisfies C1 and C2 ; and (d) σ ′ satisfies {α1 <:s τ1 , α2 =s τ1 }. Define σ ′′ = {α1 7→
sg , α2 7→ sg } ∪ σ ∪ σ1 ∪ σ2 , where sg ∈ D. Moreover, define σ ′ = σ ′′ ∪ {τ1 7→ sg } if τ1 ∈ V and σ ′ = σ ′′
otherwise. Conditions (a), (b), (c) and (d) are obviously satisfied. Thus, we see that (σ ′ , wt) is a solution
for (Γ, (a1 ≺≺[τ1 ] a2 ), wt,C).
The constraint resolution algorithm always terminates. More formally:
Theorem 4.5 (Termination of algorithm).
1. the algorithm halts, either by failing or by returning a substitution, for all C;
2. if the algorithm returns σ , then σ is a solution for C;
We can already sketch a proof of Theorem 4.5 following Pierce [15].
Proof. For part 1, define the degree of a constraint set C to be the pair (m, n), where m is the number of
constraints in C and n is the number of subtyping constraints in C. The algorithm terminates immediately
(with success in the case of an empty constraint set or failure for an equation involving two different
decorated sorts) or makes recursive calls to itself with a constraint set of lexicographically smaller degree.
For part 2, by induction on the number of recursive calls in the computation of the algorithm.

5

Conclusion

In this paper we have presented a type system for the pattern matching constructs of Tom. The system
is composed of type checking and type inference algorithms with subtyping over sorts. Since Tom also
implements associative pattern matching over variadic operators, we were interested in defining both a
way to distinguish these from syntactic operators and checking and inferring their types.
We have obtained the following: our type inference system is sound and complete w.r.t. checking,
showed by Theorems 4.4 and 4.2. This is the first step towards an effective implementation, thus leading
to a safer Tom. However, we still need to investigate type unicity that we believe to hold under our
assumptions of non-overloading and non-multiple inheritance.
As we have considered a subset of the Tom language, future work will focus on extending the type
system to handle the other constructions of the language such as anti-patterns [12, 13]. As a slightly
more prospective research area, we also want parametric polymorphism over types for Tom: our type
system will therefore have to be able to handle that as well.

Acknowledgements
We would like to acknowledge the numerous discussions we had in the Protheo and Pareo teams, especially with Paul Brauner, on these topics during these last years as well as the constructive and useful
comments done by the anonymous refereees.

Claude Kirchner, Pierre-Etienne Moreau, Cláudia Tavares

63

References
[1] Alexander Aiken and Edward L. Wimmers. Solving systems of set constraints (extended abstract). In Seventh
Annual IEEE Symposium on Logic in Computer Science, pages 329–340. IEEE Computer Society Press,
1992.
[2] H. Ait-Kaci, A. Podelski, and G. Smolka. A feature constraint system for logic programming with entailment.
Theoretical Computer Science, 122(1-2):263–283, 1994.
[3] Emilie Balland. Conception d’un langage dédié à l’analyse et la transformation de programmes. PhD thesis,
Université Henri Poincaré, 2009.
[4] Emilie Balland, Claude Kirchner, and Pierre-Etienne Moreau. Formal Islands. In Michael Johnson and
Varmo Vene, editors, 11th International Conference on Algebraic Methodology and Software Technology,
volume 4019 of LNCS, pages 51–65. Springer, 2006.
[5] Gilles Barthe, Horatiu Cirstea, Claude Kirchner, and Luigi Liquori. Pure Patterns Type Systems. In Principles of Programming Languages - POPL2003, New Orleans, USA. ACM, January 2003.
[6] Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and
Carolyn L. Talcott, editors. All About Maude, volume 4350 of Lecture Notes in Computer Science. Springer,
2007.
[7] Hubert Comon. Completion of rewrite systems with membership constraints. part i: Deduction rules. Journal
of Symbolic Computation, 25(4):397–419, 1998.
[8] Duggan Dominic. Finite subtype inference with explicit polymorphism. Sci. Comput. Program., 39(1):57–92,
2001.
[9] K. Futatsugi, J. A. Goguen, J.-P. Jouannaud, and J. Meseguer. Principles of OBJ-2. In B. Reid, editor,
Proceedings 12th ACM Symp. on Principles of Programming Languages, pages 52–66. ACM, 1985.
[10] J. A. Goguen, Claude Kirchner, Hélène Kirchner, A. Mégrelis, J. Meseguer, and T. Winkler. An introduction
to OBJ-3. In J.-P. Jouannaud and S. Kaplan, editors, Proceedings 1st International Workshop on Conditional
Term Rewriting Systems, Orsay (France), volume 308 of Lecture Notes in Computer Science, pages 258–263.
Springer-Verlag, July 1987.
[11] Claus Hintermeier, Claude Kirchner, and Hélène Kirchner. Dynamically-typed computations for order-sorted
equational presentations. Journal of Symbolic Computation, 25(4):455–526, 19[7]98.
[12] Claude Kirchner, Radu Kopetz, and Pierre-Etienne Moreau. Anti-pattern matching. In 16th European Symposium on Programming, volume 4421 of Lecture Notes in Computer Science, pages 110–124, Braga, Portugal,
2007. Springer.
[13] Radu Kopetz. Contraintes d’anti-filtrage et programmation par réécriture. PhD thesis, Institut National
Polytechnique de Lorraine, 2008.
[14] Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences,
17:348–375, 1978.
[15] Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. Chapter 22.
[16] François Pottier. Simplifying subtyping constraints: a theory. Inf. Comput., 170(2):153–183, 2001.
[17] Steffen van Bakel and Maribel Fernández. Normalization results for typeable rewrite systems. Information
and Computation, 133(2):73–116, 1997.

