A Classical Realizability Model for a
Semantical Value Restriction

arXiv:1603.07484v2 [cs.LO] 7 Apr 2016

Rodolphe Lepigre
LAMA, UMR 5127 - CNRS
Université Savoie Mont Blanc, France
rodolphe.lepigre@univ-smb.fr

Abstract. We present a new type system with support for proofs of
programs in a call-by-value language with control operators. The proof
mechanism relies on observational equivalence of (untyped) programs. It
appears in two type constructors, which are used for specifying program
properties and for encoding dependent products. The main challenge
arises from the lack of expressiveness of dependent products due to the
value restriction. To circumvent this limitation we relax the syntactic
restriction and only require equivalence to a value. The consistency of the
system is obtained semantically by constructing a classical realizability
model in three layers (values, stacks and terms).

Introduction
In this work we consider a new type system for a call-by-value language, with
control operators, polymorphism and dependent products. It is intended to serve
as a theoretical basis for a proof assistant focusing on program proving, in a
language similar to OCaml or SML. The proof mechanism relies on dependent
products and equality types t ≡ u, where t and u are (possibly untyped) terms
of the language. Equality types are interpreted as ⊤ if the denoted equivalence
holds and as ⊥ otherwise.
In our system, proofs are written using the same language as programs. For
instance, a pattern-matching corresponds to a case analysis in a proof, and a
recursive call to the use of an induction hypothesis. A proof is first and foremost
a program, hence we may say that we follow the “program as proof” principle,
rather than the usual “proof as program” principle. In particular, proofs can be
composed as programs and with programs to form proof tactics.
Programming in our language is similar to programming in any dialect of
ML. For example, we can define the type of unary natural numbers, and the
corresponding addition function.
type nat = Z [] | S [ nat ]
let rec add n m = match n with
| Z []
→ m
| S [ nn ] → S [ add nn m ]

We can then prove properties of addition such as add Z[] n ≡ n for all n in
nat. This property can be expressed using a dependent product over nat and
an equality type.
let addZeroN n : nat : ( add Z [] n ≡ n ) = 8<

The term 8< (to be pronounced “scissors”) can be introduced whenever the
goal is derivable from the context with equational reasoning. Our first proof is
immediate since we have add Z[] n ≡ n by definition of add.
Let us now show that add n Z[] ≡ n for every n in nat. Although the
statement of this property is similar to the previous one, its proof is slightly
more complex and requires case analysis and induction.
let rec addNZero n : nat : ( add n Z [] ≡ n ) =
match n with
| Z []
→ 8<
| S [ nn ] → let r = addNZero nn in 8<

In the S[nn] case, the induction hypothesis (i.e. add nn Z[] ≡ nn) is obtained by
a recursive call. It is then used to conclude the proof using equational reasoning.
Note that in our system, programs that are considered as proofs need to go
through a termination checker. Indeed, a looping program could be used to
prove anything otherwise. The proofs addZeroN and addNZero are obviously
terminating, and hence valid.
Several difficulties arise when combining call-by-value evaluation, side-effects,
dependent products and equality over programs. Most notably, the expressiveness of dependent products is weakened by the value restriction: elimination of
dependent product can only happen on arguments that are syntactic values. In
other words, the typing rule
Γ ⊢ t : Πa:A B
Γ ⊢u:A
Γ ⊢ t u : B[a := u]
cannot be proved safe if u is not a value. This means, for example, that we
cannot derive a proof of add (add Z[] Z[]) Z[] ≡ add Z[] Z[] by applying
addNZero (which has type Πn:nat (add n Z[] ≡ n)) to add Z[] Z[] since it
is not a value. The restriction affects regular programs in a similar way. For
instance, it is possible to define a list concatenation function append with the
following type.
Πn:nat Πm:nat List(n) ⇒ List(m) ⇒ List(add n m)
However, the append function cannot be used to implement a function concatenating three lists. Indeed, this would require being able to provide append with
a non-value natural number argument of the form add n m.
Surprisingly, the equality types and the underlying observational equivalence
relation provide a solution to the lack of expressiveness of dependent products.
The value restriction can be relaxed to obtain the rule

Γ, u ≡ v ⊢ t : Πa:A B
Γ, u ≡ v ⊢ u : A
Γ, u ≡ v ⊢ t u : B[a := u]
which only requires u to be equivalent to some value v. The same idea can be
applied to every rule requiring value restriction. The obtained system is conservative over the one with the syntactic restriction. Indeed, finding a value equivalent
to a term that is already a value can always be done using the reflexivity of the
equivalence relation.
Although the idea seems simple, proving the soundness of the new typing
rules semantically is surprisingly subtle. A model is built using classical realizability techniques in which the interpretation of a type A is spread among two
sets: a set of values JAK and a set of terms JAK⊥⊥ . The former contains all values
that should have type A. For example, JnatK should contain the values of the
form S[S[...Z[]...]]. The set JAK⊥⊥ is the completion of JAK with all the
terms behaving like values of JAK (in the observational sense). To show that the
relaxation of the value restriction is sound, we need the values of JAK⊥⊥ to also
be in JAK. In other words, the completion operation should not introduce new
values. To obtain this property, we need to extend the language with a new,
non-computable instruction internalizing equivalence. This new instruction is
only used to build the model, and will not be available to the user (nor will it
appear in an implementation).
About effects and value restriction
A soundness issue related to side-effects and call-by-value evaluation arose in
the seventies with the advent of ML. The problem stems from a bad interaction
between side-effects and Hindley-Milner polymorphism. It was first formulated
in terms of references [30, section 2], and many alternative type systems were
designed (e.g. [4, 14, 15, 29]). However, they all introduced a complexity that
contrasted with the elegance and simplicity of ML’s type system (for a detailed
account, see [31, section 2] and [5, section 2]).
A simple and elegant solution was finally found by Andrew Wright in the
nineties. He suggested restricting generalization in let-bindings1 to cases where
the bound term is a syntactic value [30, 31]. In slightly more expressive type
systems, this restriction appears in the typing rule for the introduction of the
universal quantifier. The usual rule
Γ ⊢t:A
X 6∈ F V (Γ )
Γ ⊢ t : ∀X A
cannot be proved safe (in a call-by-value system with side-effects) if t is not a
syntactic value. Similarly, the elimination rule for dependent product (shown
previously) requires value restriction. It is possible to exhibit a counter-example
breaking the type safety of our system if it is omitted [13].
1

In ML the polymorphism mechanism is strongly linked with let-bindings. In OCaml
syntax, they are expressions of the form let x = u in t.

In this paper, we consider control structures, which have been shown to give
a computational interpretation to classical logic by Timothy Griffin [6]. In 1991,
Robert Harper and Mark Lillibridge found a complex program breaking the type
safety of ML extended with Lisp’s call/cc [7]. As with references, value restriction
solves the inconsistency and yields a sound type system. Instead of using control
operators like call/cc, we adopt the syntax of Michel Parigot’s λµ-calculus [24].
Our language hence contains a new binder µα t capturing the continuation in the
µ-variable α. The continuation can then be restored in t using the syntax u ∗ α2 .
In the context of the λµ-calculus, the soundness issue arises when evaluating
t (µα u) when µα u has a polymorphic type. Such a situation cannot happen
with value restriction since µα u is not a value.
Main results
The main contribution of this paper is a new approach to value restriction. The
syntactic restriction on terms is replaced by a semantical restriction expressed
in terms of an observational equivalence relation denoted (≡). Although this approach seems simple, building a model to prove soundness semantically (theorem
6) is surprisingly subtle. Subject reduction is not required here, as our model
construction implies type safety (theorem 7). Furthermore our type system is
consistent as a logic (theorem 8).
In this paper, we restrict ourselves to a second order type system but it can
easily be extended to higher-order. Types are built from two basic sorts of objects: propositions (the types themselves) and individuals (untyped terms of the
language). Terms appear in a restriction operator A ↾ t ≡ u and a membership predicate t ∈ A. The former is used to define the equality types (by taking
A = ⊤) and the latter is used to encode dependent product.
Πa:A B

:=

∀a(a ∈ A ⇒ B)

Overall, the higher-order version of our system is similar to a Curry-style HOL
with ML programs as individuals. It does not allow the definition of a type
which structure depends on a term (e.g. functions with a variable number of
arguments). Our system can thus be placed between HOL (a.k.a. Fω ) and the
pure calculus of constructions (a.k.a. CoC) in (a Curry-style and classical version
of) Barendregt’s λ-cube.
Throughout this paper we build a realizability model à la Krivine [12] based
on a call-by-value abstract machine. As a consequence, formulas are interpreted
using three layers (values, stacks and terms) related via orthogonality (definition 9). The crucial property (theorem 4) for the soundness of semantical value
restriction is that
φ⊥⊥ ∩ Λv = φ
for every set of values φ (closed under (≡)). Λv denotes the set of all values
and φ⊥ (resp. φ⊥⊥ ) the set of all stacks (resp. terms) that are compatible with
2

This was originally denoted [α]u.

every value in φ (resp. stacks in φ⊥ ). To obtain a model satisfying this property,
we need to extend our programming language with a term δv,w which reduction
depends on the observational equivalence of two values v and w.
Related work
To our knowledge, combining call-by-value evaluation, side-effects and dependent
products has never been achieved before. At least not for a dependent product
fully compatible with effects and call-by-value. For example, the Aura language
[10] forbids dependency on terms that are not values in dependent applications.
Similarly, the F ⋆ language [28] relies on (partial) let-normal forms to enforce
values in argument position. Daniel Licata and Robert Harper have defined
a notion of positively dependent types [16] which only allow dependency over
strictly positive types. Finally, in language like ATS [32] and DML [33] dependent
types are limited to a specific index language.
The system that seems the most similar to ours is NuPrl [2], although it
is inconsistent with classical reasoning. NuPrl accommodates an observational
equivalence (∼) (Howe’s “squiggle” relation [8]) similar to our (≡) relation. It
is partially reflected in the syntax of the system. Being based on a Kleene style
realizability model, NuPrl can also be used to reason about untyped terms.
The central part of this paper consists in a classical realizability model construction in the style of Jean-Louis Krivine [12]. We rely on a call-by-value presentation which yields a model in three layers (values, terms and stacks). Such a
technique has already been used to account for classical ML-like polymorphism
in call-by-value in the work of Guillaume Munch-Maccagnoni [21]3 . It is here
extended to include dependent products.
The most actively developed proof assistants following the Curry-Howard
correspondence are Coq and Agda [18,22]. The former is based on Coquand and
Huet’s calculus of constructions and the latter on Martin-Löf’s dependent type
theory [3, 17]. These two constructive theories provide dependent types, which
allow the definition of very expressive specifications. Coq and Agda do not directly give a computational interpretation to classical logic. Classical reasoning
can only be done through the definition of axioms such as the law of the excluded
middle. Moreover, these two languages are logically consistent, and hence their
type-checkers only allow terminating programs. As termination checking is a
difficult (and undecidable) problem, many terminating programs are rejected.
Although this is not a problem for formalizing mathematics, this makes programming tedious.
The TRELLYS project [1] aims at providing a language in which a consistent
core can interact with type-safe dependently-typed programming with general
recursion. Although the language defined in [1] is call-by-value and allows effect,
it suffers from value restriction like Aura [10]. The value restriction does not
appear explicitly but is encoded into a well-formedness judgement appearing as
the premise of the typing rule for application. Apart from value restriction, the
3

Our theorem 4 seems unrelated to lemma 9 in Munch-Maccagnoni’s work [21].

main difference between the language of the TRELLYS project and ours resides
in the calculus itself. Their calculus is Church-style (or explicitly typed) while
ours is Curry-style (or implicitly typed). In particular, their terms and types
are defined simultaneously, while our type system is constructed on top of an
untyped calculus.
Another similar system can be found in the work of Alexandre Miquel [20],
where propositions can be classical and Curry-style. However the rest of the language remains Church style and does not embed a full ML-like language. The
PVS system [23] is similar to ours as it is based on classical higher-order logic.
However this tool does not seem to be a programming language, but rather a
specification language coupled with proof checking and model checking utilities.
It is nonetheless worth mentioning that the undecidability of PVS’s type system
is handled by generating proof obligations. Our system will take a different approach and use a non-backtracking type-checking and type-inference algorithm.

1

Syntax, Reduction and Equivalence

The language is expressed in terms of a Krivine Abstract Machine [11], which is
a stack-based machine. It is formed using four syntactic entities: values, terms,
stacks and processes. The distinction between terms and values is specific to the
call-by-value presentation, they would be collapsed in call-by-name. We require
three distinct countable sets of variables:
– Vλ = {x, y, z...} for λ-variables,
– Vµ = {α, β, γ...} for µ-variables (also called stack variables) and
– Vι = {a, b, c...} for term variables. Term variables will be bound in formulas,
but never in terms.
We also require a countable set L = {l, l1 , l2 ...} of labels to name record fields
and a countable set C = {C, C1 , C2 ...} of constructors.
Definition 1. Values, terms, stacks and processes are mutually inductively defined by the following grammars. The names of the corresponding sets are displayed on the right.
v, w ::= x | λx t | C[v] | {li = vi }i∈I

(Λv )

t, u ::= a | v | t u | µα t | p | v.l | casev [Ci [xi ] → ti ]i∈I | δv,w
π, ρ ::= α | v.π | [t]π

(Λ)
(Π)

p, q ::= t ∗ π

(Λ × Π)

Terms and values form a variation of the λµ-calculus [24] enriched with ML-like
constructs (i.e. records and variants). For technical purposes that will become
clear later on, we extend the language with a special kind of term δv,w . It will
only be used to build the model and is not intended to be accessed directly by
the user. One may note that values and processes are terms. In particular, a
process of the form t ∗ α corresponds exactly to a named term [α]t in the most

usual presentation of the λµ-calculus. A stack can be either a stack variable, a
value pushed on top of a stack, or a stack frame containing a term on top of a
stack. These two constructors are specific to the call-by-value presentation, only
one would be required in call-by-name.
Remark 1. We enforce values in constructors, record fields, projection and case
analysis. This makes the calculus simpler because only β-reduction will manipulate the stack. We can define syntactic sugars such as the following to hide the
restriction from the programmer.
t.l := (λx x.l) t

C[t] := (λx C[x]) t

Definition 2. Given a value, term, stack or process ψ we denote F Vλ (ψ) (resp.
F Vµ (ψ), T V (ψ)) the set of free λ-variables (resp. free µ-variables, term variables) contained in ψ. We say that ψ is closed if it does not contain any free
variable of any kind. The set of closed values and the set of closed terms are
denoted Λ∗v and Λ∗ respectively.
Remark 2. A stack, and hence a process, can never be closed as they always at
least contain a stack variable.
1.1

Call-by-value reduction relation

Processes form the internal state of our abstract machine. They are to be thought
of as a term put in some evaluation context represented using a stack. Intuitively,
the stack π in the process t ∗ π contains the arguments to be fed to t. Since we
are in call-by-value the stack also handles the storing of functions while their
arguments are being evaluated. This is why we need stack frames (i.e. stacks of
the form [t]π). The operational semantics of our language is given by a relation
(≻) over processes.
Definition 3. The relation (≻) ⊆ (Λ × Π)2 is defined as the smallest relation
satisfying the following reduction rules.
tu∗π

≻

u ∗ [t]π

v ∗ [t]π
λx t ∗ v.π

≻
≻

t ∗ v.π
t[x := v] ∗ π

µα t ∗ π

≻

t[α := π] ∗ π

p∗π
{li = vi }i∈I .lk ∗ π

≻
≻

p
vk ∗ π

k∈I

caseCk [v] [Ci [xi ] → ti ]i∈I ∗ π

≻

tk [xk := v] ∗ π

k∈I

We will denote (≻+ ) its transitive closure, (≻∗ ) its reflexive-transitive closure
and (≻k ) its k-fold application.

The first three rules are those that handle β-reduction. When the abstract machine encounters an application, the function is stored in a stack-frame in order
to evaluate its argument first. Once the argument has been completely computed,
a value faces the stack-frame containing the function. At this point the function
can be evaluated and the value is stored in the stack ready to be consumed by
the function as soon as it evaluates to a λ-abstraction. A capture-avoiding substitution can then be performed to effectively apply the argument to the function.
The fourth and fifth rules rules handle the classical part of computation. When
a µ-abstraction is reached, the current stack (i.e. the current evaluation context)
is captured and substituted for the corresponding µ-variable. Conversely, when
a process is reached, the current stack is thrown away and evaluation resumes
with the process. The last two rules perform projection and case analysis in the
expected way. Note that for now, states of the form δv,w ∗ π are unaffected by
the reduction relation.
Remark 3. For the abstract machine to be simpler, we use right-to-left call-byvalue evaluation, and not the more usual left-to-right call-by-value evaluation.
Lemma 1. The reduction relation (≻) is compatible with substitutions of variables of any kind. More formally, if p and q are processes such that p ≻ q then:
– for all x ∈ Vλ and v ∈ Λv , p[x := v] ≻ q[x := v],
– for all α ∈ Vµ and π ∈ Π, p[α := π] ≻ q[α := π],
– for all a ∈ Vι and t ∈ Λ, p[a := t] ≻ q[a := t].
Consequently, if σ is a substitution for variables of any kind and if p ≻ q (resp.
p ≻∗ q, p ≻+ q, p ≻k q) then pσ ≻ qσ (resp. pσ ≻∗ qσ, pσ ≻+ qσ, pσ ≻k qσ).
Proof. Immediate case analysis on the reduction rules.
We are now going to give the vocabulary that will be used to describe some
specific classes of processes. In particular we need to identify processes that are
to be considered as the evidence of a successful computation, and those that are
to be recognised as expressing failure.
Definition 4. A process p ∈ Λ × Π is said to be:
–
–
–
–
–

final if there is a value v ∈ Λv and a stack variable α ∈ Vµ such that p = v∗α,
δ-like if there are values v, w ∈ Λv and a stack π ∈ Π such that p = δv,w ∗ π,
blocked if there is no q ∈ Λ × Π such that p ≻ q,
stuck if it is not final nor δ-like, and if for every substitution σ, pσ is blocked,
non-terminating if there is no blocked process q ∈ Λ × Π such that p ≻∗ q.

Lemma 2. Let p be a process and σ be a substitution for variables of any kind.
If p is δ-like (resp. stuck, non-terminating) then pσ is also δ-like (resp. stuck,
non-terminating).
Proof. Immediate by definition.

Lemma 3. A stuck state is of one of the following forms, where k ∈
/ I.
C[v].l ∗ π

(λx t).l ∗ π

caseλx t [Ci [xi ] → ti ]i∈I ∗ π

C[v] ∗ w.π

{li = vi }i∈I ∗ v.π

case{li =vi }i∈I [Cj [xj ] → tj ]j∈J ∗ π

caseCk [v] [Ci [xi ] → ti ]i∈I ∗ π

{li = vi }i∈I .lk ∗ π

Proof. Simple case analysis.
Lemma 4. A blocked process p ∈ Λ × Π is either stuck, final, δ-like, or of one
of the following forms.
x.l ∗ π

x ∗ v.π

casex [Ci [xi ] → ti ]i∈I ∗ π

a∗π

Proof. Straight-forward case analysis using lemma 3.
1.2

Reduction of δv,w and equivalence

The idea now is to define a notion of observational equivalence over terms using
a relation (≡). We then extend the reduction relation with a rule reducing a
state of the form δv,w ∗ π to v ∗ π if v 6≡ w. If v ≡ w then δv,w is stuck. With
this rule reduction and equivalence will become interdependent as equivalence
will be defined using reduction.
Definition 5. Given a reduction relation R, we say that a process p ∈ Λ × Π
converges, and write p ⇓R , if there is a final state q ∈ Λ × Π such that pR∗ q
(where R∗ is the reflexive-transitive closure of R). If p does not converge we say
that it diverges and write p ⇑R . We will use the notations p ⇓i and p ⇑i when
working with indexed notation symbols like (։i ).
Definition 6. For every natural number i we define a reduction relation (։i )
and an equivalence relation (≡i ) which negation will be denoted (6≡i ).
(։i ) = (≻) ∪ {(δv,w ∗ π, v ∗ π) | ∃j < i, v 6≡j w}
(≡i ) = {(t, u) | ∀j ≤ i, ∀π, ∀σ, tσ ∗ π ⇓j ⇔ uσ ∗ π ⇓j }
It is easy to see that (։0 ) = (≻). For every natural number i, the relation (≡i ) is
indeed an equivalence relation as it can be seen as an intersection of equivalence
relations. Its negation can be expressed as follows.
(6≡i ) = {(t, u), (u, t) | ∃j ≤ i, ∃π, ∃σ, tσ ∗ π ⇓j ∧ uσ ∗ π ⇑j }
Definition 7. We define a reduction relation (։) and an equivalence relation
(≡) which negation will be denoted (6≡).
[
\
(։) =
(։i )
(≡) =
(≡i )
i∈N

i∈N

These relations can be expressed directly (i.e. without the need of a union or an
intersection) in the following way.
(≡) = {(t, u) | ∀i, ∀π, ∀σ, tσ ∗ π ⇓i ⇔ uσ ∗ π ⇓i }
(6≡) = {(t, u), (u, t) | ∃i, ∃π, ∃σ, tσ ∗ π ⇓i ∧ uσ ∗ π ⇑i }
(։) = (≻) ∪ {(δv,w ∗ π, v ∗ π) | v 6≡ w}
Remark 4. Obviously (։i ) ⊆ (։i+1 ) and (≡i+1 ) ⊆ (≡i ). As a consequence
the construction of (։i )i∈N and (≡i )i∈N converges. In fact (։) and (≡) form a
fixpoint at ordinal ω. Surprisingly, this property is not explicitly required.
Theorem 1. Let t and u be terms. If t ≡ u then for every stack π ∈ Π and
substitution σ we have tσ ∗ π ⇓։ ⇔ uσ ∗ π ⇓։ .
Proof. We suppose that t ≡ u and we take π0 ∈ Π and a substitution σ0 .
By symmetry we can assume that tσ0 ∗ π0 ⇓։ and show that uσ0 ∗ π0 ⇓։ . By
definition there is i0 ∈ N such that tσ0 ∗ π0 ⇓i0 . Since t ≡ u we know that for
every i ∈ N, π ∈ Π and substitution σ we have tσ ∗ π ⇓i ⇔ uσ ∗ π ⇓i . This is
true in particular for i = i0 , π = π0 and σ = σ0 . We hence obtain uσ0 ∗ π0 ⇓i0
which give us uσ0 ∗ π0 ⇓։ .
Remark 5. The converse implication is not true in general: taking t = δλx x,{}
and u = λx x gives a counter-example. More generally p ⇓։ ⇔ q ⇓։ does not
necessarily imply p ⇓i ⇔ q ⇓i for all i ∈ N.
Corollary 1. Let t and u be terms and π be a stack. If t ≡ u and t ∗ π ⇓։ then
u ∗ π ⇓։ .
Proof. Direct consequence of theorem 1 using π and an empty substitution.
1.3

Extensionality of the language

In order to be able to work with the equivalence relation (≡), we need to check
that it is extensional. In other words, we need to be able to replace equals by
equals at any place in terms without changing their observed behaviour. This
property is summarized in the following two theorems.
Theorem 2. Let v and w be values, E be a term and x be a λ-variable. If v ≡ w
then E[x := v] ≡ E[x := w].
Proof. We are going to prove the contrapositive so we suppose E[x := v] 6≡
E[x := w] and show v 6≡ w. By definition there is i ∈ N, π ∈ Π and a substitution
σ such that (E[x := v])σ ∗ π ⇓i and (E[x := w])σ ∗ π ⇑i (up to symmetry). Since
we can rename x in such a way that it does not appear in dom(σ), we can
suppose Eσ[x := vσ] ∗ π ⇓i and Eσ[x := wσ] ∗ π ⇑i . In order to show v 6≡ w we
need to find i0 ∈ N, π0 ∈ Π and a substitution σ0 such that vσ0 ∗ π0 ⇓i0 and
wσ0 ∗ π0 ⇑i0 (up to symmetry). We take i0 = i, π0 = [λx Eσ]π and σ0 = σ.
These values are suitable since by definition vσ0 ∗ π0 ։i0 Eσ[x := vσ] ∗ π ⇓i0
and wσ0 ∗ π0 ։i0 Eσ[x := wσ] ∗ π ⇑i0 .

Lemma 5. Let s be a process, t be a term, a be a term variable and k be a
natural number. If s[a := t] ⇓k then there is a blocked state p such that s ≻∗ p
and either
– p = v ∗ α for some value v and a stack variable α,
– p = a ∗ π for some stack π,
– k > 0 and p = δ(v, w) ∗ π for some values v and w and stack π, and in this
case v[a := t] 6≡j w[a := t] for some j < k.
Proof. Let σ be the substitution [a := t]. If s is non-terminating, lemma 2 tells
us that sσ is also non-terminating, which contradicts sσ ⇓k . Consequently, there
is a blocked process p such that s ≻∗ p since (≻) ⊆ (։k ). Using lemma 1 we get
sσ ≻∗ pσ from which we obtain pσ ⇓k . The process p cannot be stuck, otherwise
pσ would also be stuck by lemma 2, which would contradict pσ ⇓k . Let us now
suppose that p = δv,w ∗ π for some values v and w and some stack π. Since
δvσ,wσ ∗ π ⇓k there must be i < k such that vσ 6≡j wσ, otherwise this would
contradict δvσ,wσ ∗ π ⇓k . In this case we necessarily have k > 0, otherwise there
would be no possible candidate for i. According to lemma 4 we need to rule out
four more forms of therms: x.l ∗ π, x ∗ v.π, casex B ∗ π and b ∗ π in the case
where b 6= a. If p was of one of these forms the substitution σ would not be able
to unblock the reduction of p, which would contradict again pσ ⇓k .
Lemma 6. Let t1 , t2 and E be terms and a be a term variable. For every k ∈ N,
if t1 ≡k t2 then E[a := t1 ] ≡k E[a := t2 ].
Proof. Let us take k ∈ N, suppose that t1 ≡k t2 and show that E[a := t1 ] ≡k
E[a := t1 ]. By symmetry we can assume that we have i ≤ k, π ∈ Π and a
substitution σ such that (E[a := t1 ])σ ∗ π ⇓i and show that (E[a := t2 ])σ ∗ π ⇓i .
As we are free to rename a, we can suppose that it does not appear in dom(σ),
T V (π), T V (t1 ) or T V (t2 ). In order to lighten the notations we define E ′ = Eσ,
σ1 = [a := t1 σ] and σ2 = [a := t2 σ]. We are hence assuming E ′ σ1 ∗ π ⇓i and trying
to show E ′ σ2 ∗ π ⇓i .
We will now build a sequence (Ei , πi , li )i∈I in such a way that E ′ σ1 ∗ π ։∗k
Ei σ1 ∗ πi σ1 in li steps for every i ∈ I. Furthermore, we require that (li )i∈I is
increasing and that it has a strictly increasing subsequence. Under this condition
our sequence will necessarily be finite. If it was infinite the number of reduction
steps that could be taken from the state E ′ σ1 ∗ π would not be bounded, which
would contradict E ′ σ1 ∗ π ⇓i . We now denote our finite sequence (Ei , πi , li )i≤n
with n ∈ N. In order to show that (li )i≤n has a strictly increasing subsequence,
we will ensure that it does not have three equal consecutive values. More formally,
we will require that if 0 < i < n and li−1 = li then li+1 > li .
To define (E0 , π0 , l0 ) we consider the reduction of E ′ ∗ π. Since we know
that (E ′ ∗ π)σ1 = E ′ σ1 ∗ π ⇓i we use lemma 5 to obtain a blocked state p such
that E ′ ∗ π ≻j p. We can now take E0 ∗ π0 = p and l0 = j. By lemma 1 we
have (E ′ ∗ π)σ1 ≻j E0 σ1 ∗ π0 σ1 from which we can deduce that (E ′ ∗ π)σ1 ։∗k
E0 σ1 ∗ π0 σ1 in l0 = j steps.

To define (Ei+1 , πi+1 , li+1 ) we consider the reduction of the process Ei σ1 ∗ πi .
By construction we know that E ′ σ1 ∗ π ։∗k Ei σ1 ∗ πi σ1 = (Ei σ1 ∗ πi )σ1 in li
steps. Using lemma 5 we know that Ei ∗ πi might be of three shapes.
– If Ei ∗ πi = v ∗ α for some value v and stack variable α then the end of the
sequence was reached with n = i.
– If Ei = a then we consider the reduction of Ei σ1 ∗πi . Since (Ei σ1 ∗πi )σ1 ⇓k we
know from lemma 5 that there is a blocked process p such that Ei σ1 ∗ πi ≻j p.
Using lemma 1 we obtain that Ei σ1 ∗ πi σ1 ≻j pσ1 from which we can deduce
that Ei σ1 ∗ πi σ1 ։k pσ1 in j steps. We then take Ei+1 ∗ πi+1 = p and
li+1 = li + j.
Is it possible to have j = 0? This can only happen when Ei σ1 ∗ πi is of one
of the three forms of lemma 5. It cannot be of the form a ∗ π as we assumed
that a does not appear in t1 or σ. If it is of the form v ∗ α, then we reached
the end of the sequence with i + 1 = n so there is no trouble. The process
Ei σ1 ∗ πi may be of the form δ(v, w) ∗ π, but we will have li+2 > li+1 .
– If Ei = δ(v, w) for some values v and w we have m < k such that vσ1 6≡m
wσ1 . Hence Ei σ1 ∗ πi = δ(vσ1 , wσ1 ) ∗ πi ։k vσ1 ∗ πi by definition. Moreover
Ei σ1 ∗ πi σ1 ։k vσ1 ∗ πi σ1 by lemma 1. Since E ′ σ1 ∗ π ։∗k Ei σ1 ∗ πi σ1 in li
steps we obtain that E ′ σ1 ∗ π ։∗k vσ1 ∗ πi σ1 in li + 1 steps. This also gives
us (vσ1 ∗ πi )σ1 = vσ1 ∗ πi σ1 ⇓k .
We now consider the reduction of the process vσ1 ∗ πi . By lemma 5 there
is a blocked process p such that vσ1 ∗ πi ≻j p. Using lemma 1 we obtain
vσ1 ∗ πi σ1 ≻j pσ1 from which we deduce that vσ1 ∗ πi σ1 ։∗k pσ1 in j steps.
We then take Ei+1 ∗ πi+1 = p and li+1 = li + j + 1. Note that in this case
we have li+1 > li .
Intuitively (Ei , πi , li )i≤n mimics the reduction of E ′ σ1 ∗ π while making explicit
every substitution of a and every reduction of a δ-like state.
To end the proof we show that for every i ≤ n we have Ei σ2 ∗ πi σ2 ⇓k .
For i = 0 this will give us E ′ σ2 ∗ π ⇓k which is the expected result. Since
En ∗ πn = v ∗ α we have En σ2 ∗ πn σ2 = vσ2 ∗ α from which we trivially obtain
En σ2 ∗ πn σ2 ⇓k . We now suppose that Ei+1 σ2 ∗ πi σ2 ⇓k for 0 ≤ i < n and show
that Ei σ2 ∗ πi σ2 ⇓k . By construction Ei ∗ πi can be of two shapes4 :
– If Ei = a then t1 σ ∗ πi ։∗k Ei+1 ∗ πi+1 . Using lemma 1 we obtain t1 σ ∗
πi σ2 ։k Ei+1 σ2 ∗ πi σ2 from which we deduce t1 σ ∗ πi σ2 ⇓k by induction
hypothesis. Since t1 ≡k t2 we obtain t2 σ ∗ πi σ2 = (Ei ∗ πi )σ2 ⇓k .
– If Ei = δ(v, w) then v ∗ πi ։k Ei+1 ∗ πi+1 and hence vσ2 ∗ πi σ2 ։k Ei+1 σ2 ∗
πi+1 σ2 by lemma 1. Using the induction hypothesis we obtain vσ2 ∗ πi σ2 ⇓k .
It remains to show that δ(vσ2 , wσ2 ) ∗ πi σ2 ։∗k vσ2 ∗ πi σ2 . We need to find
j < k such that vσ2 6≡j wσ2 . By construction there is m < k such that
vσ1 6≡m wσ1 . We are going to show that vσ2 6≡m wσ2 . By using the global
induction hypothesis twice we obtain vσ1 ≡m vσ2 and wσ1 ≡m vσ2 . Now
if vσ2 ≡m wσ2 then vσ1 ≡m vσ2 ≡m wσ2 ≡m wσ1 contradicts vσ1 6≡ wσ1 .
Hence we must have vσ2 6≡m wσ2 .
4

Only En ∗ πn can be of the form v ∗ α.

Theorem 3. Let t1 , t2 and E be three terms and a be a term variable. If t1 ≡ t2
then E[a := t1 ] ≡ E[a := t2 ].
Proof. We suppose that t1 ≡ t2 which means that t1 ≡i t2 for every i ∈ N.
We need to show that E[a := t1 ] ≡ E[a := t2 ] so we take i0 ∈ N and show
E[a := t1 ] ≡i0 E[a := t2 ]. By hypothesis we have t1 ≡i0 t2 and hence we can
conclude using lemma 6.

2

Formulas and Semantics

The syntax presented in the previous section is part of a realizability machinery
that will be built upon here. We aim at obtaining a semantical interpretation of
the second-order type system that will be defined shortly. Our abstract machine
slightly differs from the mainstream presentation of Krivine’s classical realizability which is usually call-by-name. Although call-by-value presentations have
rarely been published, such developments are well-known among classical realizability experts. The addition of the δ instruction and the related modifications
are however due to the author.
2.1

Pole and orthogonality

As always in classical realizability, the model is parametrized by a pole, which
serves as an exchange point between the world of programs and the world of
execution contexts (i.e. stacks).
Definition 8. A pole is a set of processes ⊥⊥ ⊆ Λ × Π which is saturated (i.e.
closed under backward reduction). More formally, if we have q ∈ ⊥⊥ and p ։ q
then p ∈ ⊥⊥.
Here, for the sake of simplicity and brevity, we are only going to use the pole
⊥⊥ = {p ∈ Λ × Π | p ⇓։ }
which is clearly saturated. Note that this particular pole is also closed under the
reduction relation (։), even though this is not a general property. In particular
⊥⊥ contains all final processes.
The notion of orthogonality is central in Krivine’s classical realizability. In
this framework a type is interpreted (or realized) by programs computing corresponding values. This interpretation is spread in a three-layered construction,
even though it is fully determined by the first layer (and the choice of the pole).
The first layer consists of a set of values that we will call the raw semantics.
It gathers all the syntactic values that should be considered as having the corresponding type. As an example, if we were to consider the type of natural
numbers, its raw semantics would be the set {n̄ | n ∈ N} where n̄ is some encoding of n. The second layer, called falsity value is a set containing every stack
that is a candidate for building a valid process using any value from the raw
semantics. The notion of validity depends on the choice of the pole. Here for

instance, a valid process is a normalizing one (i.e. one that reduces to a final
state). The third layer, called truth value is a set of terms that is built by iterating the process once more. The formalism for the two levels of orthogonality
is given in the following definition.
Definition 9. For every set φ ⊆ Λv we define a set φ⊥ ⊆ Π and a set φ⊥⊥ ⊆ Λ
as follows.
φ⊥ = {π ∈ Π | ∀v ∈ φ, v ∗ π ∈ ⊥⊥}
φ⊥⊥ = {t ∈ Λ | ∀π ∈ φ⊥ , t ∗ π ∈ ⊥⊥}
We now give two general properties of orthogonality that are true in every
classical realizability model. They will be useful when proving the soundness of
our type system.
Lemma 7. If φ ⊆ Λv is a set of values, then φ ⊆ φ⊥⊥ .
Proof. Immediate following the definition of φ⊥⊥ .
Lemma 8. Let φ ⊆ Λv and ψ ⊆ Λv be two sets of values. If φ ⊆ ψ then
φ⊥⊥ ⊆ ψ ⊥⊥ .
Proof. Immediate by definition of orthogonality.
The construction involving the terms of the form δv,x and (≡) in the previous
section is now going to gain meaning. The following theorem, which is our central
result, does not hold in every classical realizability model. Obtaining a proof
required us to internalize observational equivalence, which introduces a noncomputable reduction rule.
Theorem 4. If Φ ⊆ Λv is a set of values closed under (≡), then Φ⊥⊥ ∩ Λv = Φ.
Proof. The direction Φ ⊆ Φ⊥⊥ ∩ Λv is straight-forward using lemma 7. We are
going to show that Φ⊥⊥ ∩ Λv ⊆ Φ, which amounts to showing that for every
value v ∈ Φ⊥⊥ we have v ∈ Φ. We are going to show the contrapositive, so let
us assume v 6∈ Φ and show v 6∈ Φ⊥⊥ . We need to find a stack π0 such that
v ∗ π0 6∈ ⊥⊥ and for every value w ∈ Φ, w ∗ π0 ∈ ⊥⊥. We take π0 = [λx δx,v ] α and
show that is is suitable. By definition of the reduction relation v ∗ π0 reduces to
δv,v ∗ α which is not in ⊥⊥ (it is stuck as v ≡ v by reflexivity). Let us now take
w ∈ Φ. Again by definition, w ∗ π0 reduces to δw,v ∗ α, but this time we have
w 6≡ v since Φ was supposed to be closed under (≡) and v 6∈ Φ. Hence w ∗ π0
reduces to w ∗ α ∈ ⊥⊥.
It is important to check that the pole we chose does not yield a degenerate
model. In particular we check that no term is able to face every stacks. If it were
the case, such a term could be use as a proof of ⊥.
Theorem 5. The pole ⊥⊥ is consistent, which means that for every closed term
t there is a stack π such that t ∗ π 6∈ ⊥⊥.

Proof. Let t be a closed term and α be a stack constant. If we do not have t∗α ⇓։
then we can directly take π = α. Otherwise we know that t ∗ α ։∗ v ∗ α for some
value v. Since t is closed α is the only available stack variable. We now show
that π = [λx {}]{}.β is suitable. We denote σ the substitution [α := π]. Using a
trivial extension of lemma 1 to the (։) relation we obtain t ∗ π = (t ∗ α)σ ։∗
(v ∗ α)σ = vσ ∗ π. We hence have t ∗ π ։∗ vσ ∗ [λx {}]{}.β ։2 {} ∗ {}.β 6∈ ⊥⊥.

2.2

Formulas and their semantics

In this paper we limit ourselves to second-order logic, even though the system
can easily be extended to higher-order. For every natural number n we require
a countable set Vn = {Xn , Yn , Zn ...} of n-ary predicate variables.
Definition 10. The syntax of formulas is given by the following grammar.
A, B ::= Xn (t1 , ..., tn ) | A ⇒ B | ∀a A | ∃a A | ∀Xn A | ∃Xn A
| {li : Ai }i∈I | [Ci : Ai ]i∈I | t ∈ A | A ↾ t ≡ u
Terms appear in several places in formulas, in particular, they form the individuals of the logic. They can be quantified over and are used as arguments
for predicate variables. Besides the ML-like formers for sums and products (i.e.
records and variants) we add a membership predicate and a restriction operation. The membership predicate t ∈ A is used to express the fact that the term t
has type A. It provides a way to encode the dependent product type using universal quantification and the arrow type. In this sense, it is inspired and related
to Krivine’s relativization of quantifiers.
Πa:A B

:=

∀a(a ∈ A ⇒ B)

The restriction operator can be thought of as a kind of conjunction with no
algorithmic content. The formula A ↾ t ≡ u is to be interpreted in the same way
as A if the equivalence t ≡ u holds, and as ⊥ otherwise5 . In particular, we will
define the following types:
A ↾ t 6≡ u := A ↾ t ≡ u ⇒ ⊥

t ≡ u := ⊤ ↾ t ≡ u

t 6≡ u := ⊤ ↾ t 6≡ u

To handle free variables in formulas we will need to generalize the notion of
substitution to allow the substitution of predicate variables.
Definition 11. A substitution is a finite map σ ranging over λ-variables, µvariables, term and predicate variables such that:
– if x ∈ dom(σ) then σ(x) ∈ Λv ,
– if α ∈ dom(σ) then σ(α) ∈ Π,
– if a ∈ dom(σ) then σ(a) ∈ Λ,
5

We use the standard second-order encoding: ⊥ = ∀X0 X0 and ⊤ = ∃X0 X0 .

– if Xn ∈ dom(σ) then σ(Xn ) ∈ Λn → P(Λv /≡).
Remark 6. A predicate variable of arity n will be substituted by a n-ary predicate. Semantically, such predicate will correspond to some total (set-theoretic)
function building a subset of Λv /≡ from n terms. In the syntax, the binding of
the arguments of a predicate variables will happen implicitly during its substitution.
Definition 12. Given a formula A we denote F V (A) the set of its free variables.
Given a substitution σ such that F V (A) ⊆ dom(σ) we write A[σ] the closed
formula built by applying σ to A.
In the semantics we will interpret closed formulas by sets of values closed
under the equivalence relation (≡).
Definition 13. Given a formula A and a substitution σ such that A[σ] is closed,
we define the raw semantics JAKσ ⊆ Λv / ≡ of A under the substitution σ as
follows.
JXn (t1 , ..., tn )Kσ = σ(Xn )(t1 σ, ..., tn σ)
JA ⇒ BKσ = {λx t | ∀v ∈ JAKσ , t[x := v] ∈ JBK⊥⊥
σ }
J∀a AKσ = ∩t∈Λ∗ JAKσ[a:=t]
J∃a AKσ = ∪t∈Λ∗ JAKσ[a:=t]
J∀Xn AKσ = ∩P ∈Λn →P(Λv /≡) JAKσ[Xn :=P ]
J∃Xn AKσ = ∪P ∈Λn →P(Λv /≡) JAKσ[Xn :=P ]
J{li : Ai }i∈I Kσ = {{li = vi }i∈I | ∀i ∈ I vi ∈ JAi Kσ }
J[Ci : Ai ]i∈I Kσ = ∪i∈I {Ci [v] | v ∈ JAi Kσ }
Jt ∈ AKσ = {v ∈ JAKσ | tσ ≡ v}

JAKσ if tσ ≡ uσ
JA ↾ t ≡ uKσ =
∅
otherwise
In the model, programs will realize closed formulas in two different ways
according to their syntactic class. The interpretation of values will be given in
terms of raw semantics, and the interpretation of terms in general will be given
in terms of truth values.
Definition 14. Let A be a formula and σ a substitution such that A[σ] is closed.
We say that:
– v ∈ Λv realizes A[σ] if v ∈ JAKσ ,
– t ∈ Λ realizes A[σ] if t ∈ JAK⊥⊥
σ .
2.3

Contexts and typing rules

Before giving the typing rules of our system we need to define contexts and
judgements. As explained in the introduction, several typing rules require a
value restriction in our context. This is reflected in typing rule by the presence
of two forms of judgements.

Definition 15. A context is an ordered list of hypotheses. In particular, it contains type declarations for λ-variables and µ-variables, and declaration of term
variables and predicate variables. In our case, a context also contains term equivalences and inequivalences. A context is built using the following grammar.
Γ, ∆ ::= • | Γ, x : A | Γ, α : ¬A | Γ, a : T erm
| Γ, Xn : P redn | Γ, t ≡ u | Γ, t 6≡ u
A context Γ is said to be valid if it is possible to derive Γ Valid using the rules
of figure 1. In the following, every context will be considered valid implicitly.

Γ Valid

x 6∈ dom(Γ )
F V (A) ⊆ dom(Γ ) ∪ {x}
Γ, x : A Valid

Γ Valid

α 6∈ dom(Γ )
F V (A) ⊆ dom(Γ )
Γ, α : ¬A Valid

Γ Valid
a 6∈ dom(Γ )
Γ, a : T erm Valid
Γ Valid

Γ Valid

Γ Valid
Xn 6∈ dom(Γ )
Γ, Xn : P redn Valid

F V (t) ∪ F V (u) ⊆ dom(Γ )
Γ, t ≡ u Valid

F V (t) ∪ F V (u) ⊆ dom(Γ )
Γ, t 6≡ u Valid

• Valid

Fig. 1. Rules allowing the construction of a valid context.

Definition 16. There are two forms of typing judgements:
– Γ ⊢val v : A meaning that the value v has type A in context Γ ,
– Γ ⊢ t : A meaning that the term t has type A in context Γ .
The typing rules of the system are given in figure 2. Although most of them
are fairly usual, our type system differs in several ways. For instance the last four
rules are related to the extensionality of the calculus. One can note the value
restriction in several places: both universal quantification introduction rules and
the introduction of the membership predicate. In fact, some value restriction is
also hidden in the rules for the elimination of the existential quantifiers and the
elimination rule for the restriction connective. These rules are presented in their
left-hand side variation, and only values can appear on the left of the sequent.
It is not surprising that elimination of an existential quantifier requires value
restriction as it is the dual of the introduction rule of a universal quantifier.

Γ, x : A ⊢val x : A

Γ ⊢val v : A
↑
Γ ⊢v:A

ax

Γ ⊢v:A ↓
Γ ⊢val v : A
Γ, x : A ⊢ t : B
⇒i
Γ ⊢val λx t : A ⇒ B

Γ ⊢t:A⇒B
Γ ⊢ u : A ⇒e
Γ ⊢tu:B
Γ, α : ¬A ⊢ t : A
µ
Γ ⊢ µα t : A

Γ, α : ¬A ⊢ t : A
∗
Γ, α : ¬A ⊢ t ∗ α : B
Γ, x : A, x ≡ u ⊢ t : A
∈e
Γ, x : u ∈ A ⊢ t : A

Γ ⊢val v : A
∈i
Γ ⊢val v : v ∈ A
Γ, u1 ≡ u2 ⊢ t : A
↾i
Γ, u1 ≡ u2 ⊢ t : A ↾ u1 ≡ u2

Γ, x : A, u1 ≡ u2 ⊢ t : B
↾e
Γ, x : A ↾ u1 ≡ u2 ⊢ t : B

Γ ⊢val v : A
a 6∈ F V (Γ )
∀i
Γ ⊢val v : ∀a A

Γ ⊢ t : ∀a A
∀e
Γ ⊢ t : A[a := u]

Γ, y : A ⊢ t : B
a 6∈ F V (Γ, B) ∪ T V (t)
∃e
Γ, y : ∃a A ⊢ t : B

Γ ⊢ t : A[a := u]
∃i
Γ ⊢ t : ∃a A

Γ ⊢val v : A
Xn 6∈ F V (Γ )
∀I
Γ ⊢val v : ∀Xn A

Γ ⊢ t : ∀Xn A
∀E
Γ ⊢ t : A[Xn := P ]

Γ, x : A ⊢ t : B
Xn 6∈ F V (Γ, B)
∃E
Γ, x : ∃Xn A ⊢ t : B

Γ ⊢ t : A[Xn := P ]
∃I
Γ ⊢ t : ∃Xn A

[Γ ⊢val vi : Ai ]1≤i≤n
×i
Γ ⊢val {li = vi }n
i=1 : {li : Ai }1≤i≤n

Γ ⊢val v : {li : Ai }1≤i≤n
×e
Γ ⊢ v.li : Ai

Γ ⊢val v : Ai
+i
Γ ⊢val Ci [v] : [Ci : Ai ]1≤i≤n
Γ ⊢val v : [Ci : Ai ]1≤i≤n
[Γ, x : Ai , Ci [x] ≡ v ⊢ ti : B]1≤i≤n
+e
Γ ⊢ casev [Ci [x] → ti ]1≤i≤n : B
Γ, w1 ≡ w2 ⊢ t[x := w1 ] : A
≡v,l
Γ, w1 ≡ w2 ⊢ t[x := w2 ] : A
Γ, w1 ≡ w2 ⊢ t : A[x := w1 ]
≡v,r
Γ, w1 ≡ w2 ⊢ t : A[x := w2 ]

Γ, t1 ≡ t2 ⊢ t[a := t1 ] : A
≡t,l
Γ, t1 ≡ t2 ⊢ t[a := t2 ] : A
Γ, t1 ≡ t2 ⊢ t : A[a := t1 ]
≡t,r
Γ, t1 ≡ t2 ⊢ t : A[a := t2 ]

Fig. 2. Second-order type system.

An important and interesting difference with existing type systems is the
presence of ↑ and ↓. These two rules allow one to go from one kind of sequent
to the other when working on values. Going from Γ ⊢val v : A to Γ ⊢ v : A is
straight-forward. Going the other direction is the main motivation for our model.
This allows us to lift the value restriction expressed in the syntax to a restriction
expressed in terms of equivalence. For example, the two rules
Γ, t ≡ v ⊢ t : A
a 6∈ F V (Γ )
∀i,≡
Γ, t ≡ v ⊢ t : ∀a A
Γ, u ≡ v ⊢ t : Πa:A B
Γ, u ≡ v ⊢ u : A
Πe,≡
Γ, u ≡ v ⊢ t u : B[a := u]
can be derived in the system (see figure 3). The value restriction can be removed
similarly on every other rule. Thus, judgements on values can be completely
ignored by the user of the system. Transition to value judgements will only
happen internally.
Γ, t ≡ v ⊢ t : A
≡t,l
Γ, t ≡ v ⊢ v : A
↓
Γ, t ≡ v ⊢val v : A
a 6∈ F V (Γ )
∀i
Γ, t ≡ v ⊢val v : ∀a A
↑
Γ, t ≡ v ⊢ v : ∀a A
≡t,l
Γ, t ≡ v ⊢ t : ∀a A
Γ, u ≡ v ⊢ u : A
≡t,l
Γ, u ≡ v ⊢ v : A
↓
Γ, u ≡ v ⊢val v : A
∈i
Γ, u ≡ v ⊢val v : v ∈ A
↑
Γ, u ≡ v ⊢ t : Πa:AB
Γ, u ≡ v ⊢ v : v ∈ A
≡t,l
Γ, u ≡ v ⊢ t : ∀a(a ∈ A ⇒ B)
Γ, u ≡ v ⊢ u : v ∈ A
≡t,r
∀e
Γ, u ≡ v ⊢ t : u ∈ A ⇒ B[a := u]
Γ, u ≡ v ⊢ u : u ∈ A
⇒e
Γ, u ≡ v ⊢ t u : B[a := u]
Fig. 3. Derivation of the rules ∀i,≡ and Πe,≡ .

2.4

Adequacy

We are now going to prove the soundness of our type system by showing that
it is compatible with our realizability model. This property is specified by the
following theorem which is traditionally called the adequacy lemma.
Definition 17. Let Γ be a (valid) context. We say that the substitution σ realizes Γ if:

–
–
–
–
–
–

for
for
for
for
for
for

every
every
every
every
every
every

x : A in Γ we have σ(x) ∈ JAKσ ,
α : ¬A in Γ we have σ(α) ∈ JAK⊥
σ,
a : T erm in Γ we have σ(a) ∈ Λ,
Xn : P redn in Γ we have σ(Xn ) ∈ Λn → Λv /≡,
t ≡ u in Γ we have tσ ≡ uσ and
t 6≡ u in Γ we have tσ 6≡ uσ.

Theorem 6. (Adequacy.) Let Γ be a (valid) context, A be a formula such that
F V (A) ⊆ dom(Γ ) and σ be a substitution realizing Γ .
– If Γ ⊢val v : A then vσ ∈ JAKσ ,
– if Γ ⊢ t : A then tσ ∈ JAK⊥⊥
σ .
Proof. We proceed by induction on the derivation of the judgement Γ ⊢val v : A
(resp. Γ ⊢ t : A) and we reason by case on the last rule used.
(ax) By hypothesis σ realizes Γ, x : A from which we directly obtain xσ ∈ JAKσ .
(↑) and (↓) are direct consequences of lemma 7 and theorem 4 respectively.
⊥
(⇒e ) We need to prove that tσ uσ ∈ JBK⊥⊥
σ , hence we take π ∈ JBKσ and show
tσ uσ ∗ π ∈ ⊥⊥. Since ⊥⊥ is saturated, we can take a reduction step and show
uσ ∗ [tσ]π ∈ ⊥⊥. By induction hypothesis uσ ∈ JAK⊥⊥
so we only have to show
σ
.
To
do
so
we
take
v
∈
JAK
and
show
v
∗
[tσ]π ∈ ⊥⊥. Here we can
[tσ]π ∈ JAK⊥
σ
σ
again take a reduction step and show tσ ∗ v.π ∈ ⊥⊥. By induction hypothesis we
⊥
have tσ ∈ JA ⇒ BK⊥⊥
σ , hence it is enough to show v.π ∈ JA ⇒ BKσ . We now
take a value λx tx ∈ JA ⇒ BKσ and show that λx tx ∗ v.π ∈ ⊥⊥. We then apply
again a reduction step and show tx [x := v] ∗ π ∈ ⊥⊥. Since π ∈ JBK⊥
σ we only
need to show tx [x := v] ∈ JBK⊥⊥
which
is
true
by
definition
of
JA
⇒
BKσ .
σ
(⇒i ) We need to show λx tσ ∈ JA ⇒ BKσ so we take v ∈ JAKσ and show
tσ[x := v] ∈ JBK⊥⊥
σ . Since σ[x := v] realizes Γ, x : A we can conclude using the
induction hypothesis.
(µ) We need to show that µα tσ ∈ JAK⊥⊥
hence we take π ∈ JAK⊥
σ
σ and show
µα tσ ∗ π ∈ ⊥⊥. Since ⊥⊥ is saturated, it is enough to show tσ[α := π] ∗ π ∈ ⊥⊥.
As σ[α := π] realizes Γ, α : ¬A we conclude by induction hypothesis.
⊥
(∗) We need to show tσ ∗ ασ ∈ JBK⊥⊥
σ , hence we take π ∈ JBKσ and show that
(tσ ∗ ασ) ∗ π ∈ ⊥⊥. Since ⊥⊥ is saturated, we can take a reduction step and show
hence it is enough to show
tσ ∗ ασ ∈ ⊥⊥. By induction hypothesis tσ ∈ JAK⊥⊥
σ
ασ ∈ JAK⊥
which
is
true
by
hypothesis.
σ
(∈i ) We need to show vσ ∈ Jv ∈ AKσ . We have vσ ∈ JAKσ by induction hypothesis, and vσ ≡ vσ by reflexivity of (≡).
(∈e ) By hypothesis we know that σ realizes Γ, x : u ∈ A. To be able to conclude
using the induction hypothesis, we need to show that σ realizes Γ, x : A, x ≡ u.
Since we have σ(x) ∈ Ju ∈ AKσ , we obtain that xσ ∈ JAKσ and xσ ≡ uσ by
definition of Ju ∈ AKσ .
(↾i ) We need to show tσ ∈ JA ↾ u1 ≡ u2 K⊥⊥
σ . By hypothesis u1 σ ≡ u2 σ, hence
JA ↾ u1 ≡ u2 Kσ = JAKσ . Consequently, it is enough to show that tσ ∈ JAK⊥⊥
σ ,
which is exactly the induction hypothesis.

(↾e ) By hypothesis we know that σ realizes Γ, x : A ↾ u1 ≡ u2 . To be able to use
the induction hypothesis, we need to show that σ realizes Γ, x : A, u1 ≡ u2 . Since
we have σ(x) ∈ JA ↾ u1 ≡ u2 Kσ , we obtain that xσ ∈ JAKσ and that u1 σ ≡ u2 σ
by definition of JA ↾ u1 ≡ u2 Kσ .
T
(∀i ) We need to show that vσ ∈ J∀a AKσ = t∈Λ JAKσ[a:=t] so we take t ∈ Λ and
show vσ ∈ JAKσ[a:=t] . This is true by induction hypothesis since a 6∈ F V (Γ ) and
hence σ[a := t] realizes Γ .
(∀e ) We need to show tσ ∈ JA[a := u]K⊥⊥
= JAK⊥⊥
σ
σ[a:=uσ] for some u ∈ Λ. By
⊥⊥
induction hypothesis we know tσ ∈ J∀a AKσ , hence we only need to show that
J∀a AK⊥⊥
⊆ JAK⊥⊥
σ
σ[a:=uσ] . By definition we have J∀a AKσ ⊆ JAKσ[a:=uσ] so we can
conclude using lemma 8.
(∃e ) By hypothesis we know that σ realizes Γ, x : ∃a A. In particular, we know
that σ(x) ∈ J∃a AKσ , which means that there is a term u ∈ Λ∗ such that
σ(x) ∈ JAKσ[a:=u] . Since a ∈
/ F V (Γ ), we obtain that the substitution σ[a := u]
realizes the context Γ, x : A. Using the induction hypothesis, we finally get
⊥⊥
tσ = tσ[a := u] ∈ JBK⊥⊥
since a ∈
/ T V (t) and a ∈
/ F V (B).
σ[a:=u] = JBKσ
(∃i ) The proof for this rule is similar to the one for (∀e ). We need to show that
⊥⊥
JA[a := u]K⊥⊥
= JAK⊥⊥
σ
σ[a:=uσ] ⊆ J∃a AKσ . This follows from lemma 8 since
JAKσ[a:=uσ] ⊆ J∃a AKσ by definition.
(∀I ), (∀E ), (∃E ) and (∃I ) are similar to similar to (∀i ), (∀e ), (∃e ) and (∃i ).
(×i ) We need to show that {li = vi σ}i∈I ∈ J{li : Ai }i∈I Kσ . By definition we need
to show that for all i ∈ I we have vi σ ∈ JAi Kσ . This is immediate by induction
hypothesis.
(×e ) We need to show that vσ.li ∈ JAi K⊥⊥
for some i ∈ I. By induction hypothσ
esis we have vσ ∈ J{li : Ai }i∈I Kσ and hence v has the form {li = vi }i∈I with
vi σ ∈ JAi Kσ . Let us now take π ∈ JAi K⊥
⊥.
σ and show that {li = vi σ}i∈I .li ∗ π ∈ ⊥
Since ⊥⊥ is saturated, it is enough to show vi σ ∗ π ∈ ⊥⊥. This is true since
vi σ ∈ JAi Kσ and π ∈ JAi K⊥
σ.
(+i ) We need to show Ci [vσ] ∈ J[Ci : Ai ]i∈I Kσ for some i ∈ I. By induction
hypothesis vσ ∈ JAi Kσ and hence we can conclude by definition of J[Ci : Ai ]i∈I Kσ .
(+e ) We need to show casevσ [Ci [x] → ti σ]i∈I ∈ JBK⊥⊥
σ . By induction hypothesis
vσ ∈ J[Ci of Ai ]i∈I Kσ which means that there is i ∈ I and w ∈ JAi Kσ such that
vσ = Ci [w]. We take π ∈ JBK⊥
⊥.
σ and show caseCi [w] [Ci [x] → ti σ]i∈I ∗ π ∈ ⊥
Since ⊥⊥ is saturated, it is enough to show ti σ[x := w] ∗ π ∈ ⊥⊥. It remains to
show that ti σ[x := w] ∈ JBK⊥⊥
σ . To be able to conclude using the induction
hypothesis we need to show that σ[x := w] realizes Γ, x : Ai , Ci [x] ≡ v. This is
true since σ realizes Γ , w ∈ JAi Kσ and Ci [w] ≡ vσ by reflexivity.
(≡v,l ) We need to show t[x := w1 ]σ = tσ[x := w1 σ] ∈ JAKσ . By hypothesis we
know that w1 σ ≡ w2 σ from which we can deduce tσ[x := w1 σ] ≡ tσ[x := w2 σ]
by extensionality (theorem 2). Since JAKσ is closed under (≡) we can conclude
using the induction hypothesis.
(≡t,l ), (≡v,r ) and (≡t,r ) are similar to (≡v,l ), using extensionality (theorem 2
and theorem 3).

Remark 7. For the sake of simplicity we fixed a pole ⊥⊥ at the beginning of the
current section. However, many of the properties presented here (including the
adequacy lemma) remain valid with similar poles. We will make use of this fact
in the proof of the following theorem.
Theorem 7. (Safety.) Let Γ be a context, A be a formula such that F V (A) ⊆
dom(Γ ) and σ be a substitution realizing Γ . If t is a term such that Γ ⊢ t : A
and if A[σ] is pure (i.e. it does not contain any ⇒ ), then for every stack
∗
π ∈ JAK⊥
σ there is a value v ∈ JAKσ and α ∈ Vµ such that tσ ∗ π ։ v ∗ α.
Proof. We do a proof by realizability using the following pole.
⊥⊥A = {p ∈ Λ × Π | p ։∗ v ∗ α ∧ v ∈ JAKσ }
It is well-defined as A is pure and hence JAKσ does not depend on the pole.
Using the adequacy lemma (theorem 6) with ⊥⊥A we obtain tσ ∈ JAK⊥⊥
σ . Hence
for every stack π ∈ JAK⊥
⊥A . We can then conclude using the
σ we have tσ ∗ π ∈ ⊥
definition of the pole ⊥⊥A .
Remark 8. It is easy to see that if A[σ] is closed and pure then v ∈ JAKσ implies
that • ⊢ v : A.
Theorem 8. (Consistency.) There is no t such that • ⊢ t : ⊥.
Proof. Let us suppose that • ⊢ t : ⊥. Using adequacy (theorem 6 ) we obtain
⊥
that t ∈ J⊥K⊥⊥
σ . Since J⊥Kσ = ∅ we know that J⊥Kσ = Π by definition. Now
using theorem 5 we obtain J⊥K⊥⊥
=
∅.
This
is
a
contradiction.
σ

3

Deciding Program Equivalence

The type system given in figure 2 does not provide any way of discharging an
equivalence from the context. As a consequence the truth of an equivalence
cannot be used. Furthermore, an equational contradiction in the context cannot
be used to derive falsehood. To address these two problems, we will rely on a
partial decision procedure for the equivalence of terms. Such a procedure can be
easily implemented using an algorithm similar to Knuth-Bendix, provided that
we are able to extract a set of equational axioms from the definition of (≡). In
particular, we will use the following lemma to show that several reduction rules
are contained in (≡).
Lemma 9. Let t and u be terms. If for every stack π ∈ Π there is p ∈ Λ × Π
such that t ∗ π ≻∗ p and u ∗ π ≻∗ p then t ≡ u.
Proof. Since (≻) ⊆ (։i ) for every i ∈ N, we can deduce that t ∗ π ։∗i p
and u ∗ π ։∗i p for every i ∈ N. Using lemma 1 we can deduce that for every
substitution σ we have tσ ∗π ։∗i pσ and uσ ∗π ։∗i pσ for all i ∈ N. Consequently
we obtain t ≡ u.

The equivalence relation contains call-by-value β-reduction, projection on records
and case analysis on variants.
Theorem 9. For every x ∈ Vλ , t ∈ Λ and v ∈ Λv we have (λx t)v ≡ t[x := v].
Proof. Immediate using lemma 9.
Theorem 10. For all k such that 1 ≤ k ≤ n we have the following equivalences.
(λx t)v ≡ t[x := v]

caseCk [v] [Ci [xi ] → ti ]1≤i≤n ≡ tk [xk := v]

Proof. Immediate using lemma 9.
To observe contradictions, we also need to derive some inequivalences on
values. For instance, we would like to deduce a contradiction if two values with
a different head constructor are assumed to be equivalent.
Theorem 11. Let C, D ∈ C be constructors, and v, w ∈ Λv be values. If C 6= D
then C[v] 6≡ D[w].
Proof. We take π = [λx casex [C[y] → y | D[y] → Ω]]α where Ω is an arbitrary
diverging term. We then obtain C[v] ∗ π ⇓0 and D[w] ∗ π ⇑0 .
Theorem 12. Let {li = vi }i∈I and {lj = vj }j∈J be two records. If k is a index
such that k ∈ I and k ∈
/ J then we have {li = vi }i∈I 6≡ {lj = vj }j∈J .
Proof. Immediate using the stack π = [λx x.lk ]α.
Theorem 13. For every x ∈ Vλ , v ∈ Λv , t ∈ Λ, C ∈ C and for every record
{li = vi }i∈I we have the following inequivalences.
λx t 6≡ C[v]

λx t 6≡ {li = vi }i∈I

C[v] 6≡ {li = vi }i∈I

Proof. The proof is mostly similar to the proofs of the previous two theorems.
However, there is a subtlety with the second inequivalence. If for every value v
the term t[x := v] diverges, then we do not have λx t 6≡ {}. Indeed, there is no
evaluation context (or stack) that is able to distinguish the empty record {} and
a diverging function. To solve this problem, we can extend the language with a
new kind of term unitv and extend the relation (≻) with the following rule.
unit{} ∗ π

≻

{} ∗ π

The process unitv ∗ π is stuck for every value v 6= {}. The proof can the be
completed using the stack π = [λx unitx ]α.
The previous five theorems together with the extensionality of (≡) and its
properties as an equivalence relation can be used to implement a partial decision
procedure for equivalence. We will incorporate this procedure into the typing
rules by introducing a new form of judgment.

Definition 18. An equational context E is a list of hypothetical equivalences and
inequivalences. Equational contexts are built using the following grammar.
E := • | E, t ≡ u | E, t 6≡ u
Given a context Γ , we denote EΓ its restriction to an equational context.
Definition 19. Let E be an equational context. The judgement E ⊢ ⊥ is valid if
and only if the partial decision procedure is able to derive a contradiction in E.
We will write E ⊢ t ≡ u for E, t 6≡ u ⊢ ⊥ and E ⊢ t 6≡ u for E, t ≡ u ⊢ ⊥
To discharge equations from the context, the following two typing rules are
added to the system.
Γ, u1 ≡ u2 ⊢ t : A
EΓ ⊢ u 1 ≡ u 2
≡
Γ ⊢t:A
Γ, u1 6≡ u2 ⊢ t : A
EΓ ⊢ u1 6≡ u2
6≡
Γ ⊢t:A
The soundness of these new rules follows easily since the decision procedure
agrees with the semantical notion of equivalence. The axioms that were given
at the beginning of this section are only used to partially reflect the semantical
equivalence relation in the syntax. This is required if we are to implement the
decision procedure.
Another way to use an equational context is to derive a contradiction directly.
For instance, if we have a context Γ such that EΓ yields a contradiction, one
should be able to finish the corresponding proof. This is particularly useful when
working with variants and case analysis. For instance, some branches of the case
analysis might not be reachable due to constraints on the matched term. For
instance, we know that in the term
caseC[v] [C[x] → x | D[x] → t]
the branch corresponding to the D constructor will never be reached. Consequently, we can replace t by any term and the computation will still behave
correctly. For this purpose we introduce a special value 8< on which the abstract
machine fails. It can be introduced with the following typing rule.
EΓ ⊢ ⊥
8<
Γ ⊢val 8< : ⊥
The soundness of this rule is again immediate.

4

Further Work

The model presented in the previous sections is intended to be used as the basis
for the design of a proof assistant based on a call-by-value ML language with
control operators. A first prototype (with a different theoretical foundation) was
implemented by Christophe Raffalli [27]. Based on this experience, the design of a
new version of the language with a clean theoretical basis can now be undertaken.
The core of the system will consist of three independent components: a typechecker, a termination checker and a decision procedure for equivalence.
Working with a Curry style language has the disadvantage of making typechecking undecidable. While most proof systems avoid this problem by switching
to Church style, it is possible to use heuristics making most Curry style programs
that arise in practice directly typable. Christophe Raffalli implemented such a
system [26] and from his experience it would seem that very little help from the
user is required in general. In particular, if a term is typable then it is possible
for the user to provide hints (e.g. the type of a variable) so that type-checking
may succeed. This can be seen as a kind of completeness.
Proof assistants like Coq [18] or Agda [22] both have decidable type-checking
algorithms. However, these systems provide mechanisms for handling implicit
arguments or meta-variables which introduce some incompleteness. This does
not make these systems any less usable in practice. We conjecture that going
even further (i.e. full Curry style) provides a similar user experience.
To obtain a practical programming language we will need support for recursive programs. For this purpose we plan on adapting Pierre Hyvernat’s termination checker [9]. It is based on size change termination and has already been
used in the first prototype implementation. We will also need to extend our type
system with inductive (and coinductive) types [19, 25]. They can be introduced
in the system using fixpoints µX A (and νX A).

Acknowledgments
I would like to particularly thank my research advisor, Christophe Raffalli, for his
guidance and input. I would also like to thank Alexandre Miquel for suggesting
the encoding of dependent products. Thank you also to Pierre Hyvernat, Tom
Hirschowitz, Robert Harper and the anonymous reviewers for their very helpful
comments.

References
1. Casinghino, C., Sjöberg, V., Weirich, S.: Combining proofs and programs in a
dependently typed language. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL ’14, San Diego, CA, USA. pp. 33–46. ACM (2014)
2. Constable, R.L., Allen, S.F., Bromley, M., Cleaveland, R., Cremer, J.F., Harper,
R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T.,

3.
4.

5.

6.

7.
8.

9.
10.

11.
12.

13.

14.
15.

16.

17.

18.
19.

Smith, S.F.: Implementing mathematics with the Nuprl proof development system.
Prentice Hall (1986)
Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2-3), 95–120
(Feb 1988)
Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 207–212. POPL ’82, ACM, New York, NY, USA (1982)
Garrigue, J.: Relaxing the value restriction. In: Kameyama, Y., Stuckey, P. (eds.)
Functional and Logic Programming, Lecture Notes in Computer Science, vol. 2998,
pp. 196–213. Springer Berlin Heidelberg (2004)
Griﬃn, T.G.: A formulæ-as-types notion of control. In: In Conference Record of the
Seventeenth Annual ACM Symposium on Principles of Programming Languages.
pp. 47–58. ACM Press (1990)
Harper, R., Lillibridge, M.: ML with callcc is unsound (Jul 1991),
http://www.seas.upenn.edu/~ sweirich/types/archive/1991/msg00034.html
Howe, D.J.: Equality in lazy computation systems. In: Proceedings of the Fourth
Annual Symposium on Logic in Computer Science (LICS ’89), Paciﬁc Grove, California, USA, June 5-8, 1989. pp. 198–203 (1989)
Hyvernat, P.: The size-change termination principle for constructor based languages. Logical Methods in Computer Science 10(1) (2014)
Jia, L., Vaughan, J.A., Mazurak, K., Zhao, J., Zarko, L., Schorr, J., Zdancewic, S.:
AURA: a programming language for authorization and audit. In: Hook, J., Thiemann, P. (eds.) Proceeding of the 13th ACM SIGPLAN international conference
on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28,
2008. pp. 27–38. ACM (2008)
Krivine, J.: A call-by-name lambda-calculus machine. Higher-Order and Symbolic
Computation 20(3), 199–207 (2007)
Krivine, J.: Realizability in classical logic. In: Interactive models of computation
and program behaviour, Panoramas et synthèses, vol. 27, pp. 197–229. Société
Mathématique de France (2009)
Lepigre, R.: A realizability model for a semantical value restriction (2015),
https://lama.univ-savoie.fr/~ lepigre/files/docs/semvalrest2015.pdf,
long version
Leroy, X.: Polymorphism by name for references and continuations. In: 20th symposium Principles of Programming Languages. pp. 220–231. ACM Press (1993)
Leroy, X., Weis, P.: Polymorphic type inference and assignment. In: Proceedings
of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages. pp. 291–302. POPL ’91, ACM, New York, NY, USA (1991)
Licata, D.R., Harper, R.: Positively dependent types. In: Altenkirch, T., Millstein,
T.D. (eds.) Proceedings of the 3rd ACM Workshop Programming Languages meets
Program Veriﬁcation, PLPV 2009, Savannah, GA, USA, January 20, 2009. pp. 3–
14. ACM (2009)
Martin-Löf, P.: Constructive mathematics and computer programming. In: Cohen,
L., Loś, J., Pfeiﬀer, H., Podewski, K.P. (eds.) Logic, Methodology and Philosophy
of Science VI, Studies in Logic and the Foundations of Mathematics, vol. 104, pp.
153–175. North-Holland (1982)
The Coq development team: The Coq proof assistant reference manual. LogiCal
Project (2004), http://coq.inria.fr, version 8.0
Mendler, N.P.: Recursive types and type constraints in second-order lambda calculus. In: Proceedings of the Symposium on Logic in Computer Science (LICS) 1987.
pp. 30–36 (1987)

20. Miquel, A.: Le Calcul des Constructions Implicites : Syntaxe et Sémantique. Ph.D.
thesis, Université Paris VII (2001)
21. Munch-Maccagnoni, G.: Focalisation and classical realisability. In: Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of
the EACSL. pp. 409–423 (2009)
22. Norell, U.: Dependently Typed Programming in Agda. In: Lecture Notes from the
Summer School in Advanced Functional Programming (2008)
23. Owre, S., Rajan, S., Rushby, J., Shankar, N., Srivas, M.: PVS: combining speciﬁcation, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.)
Computer-Aided Veriﬁcation, CAV ’96. pp. 411–414. No. 1102 in Lecture Notes in
Computer Science (1996)
24. Parigot, M.: λµ-calculus: An algorithmic interpretation of classical natural deduction. In: Lecture Notes in Computer Science, vol. 624, pp. 190–201. Springer (1992)
25. Raﬀalli, C.: L’Arithmétiques Fonctionnelle du Second Ordre avec Points Fixes.
Ph.D. thesis, Université Paris VII (1994)
26. Raﬀalli, C.: A normaliser for pure and typed λ-calculus (1996),
http://lama.univ-savoie.fr/~ raffalli/normaliser.html
27. Raﬀalli, C.: The PML programming language. LAMA - Université Savoie MontBlanc (2012), http://lama.univ-savoie.fr/tracpml/
28. Swamy, N., Chen, J., Fournet, C., Strub, P., Bhargavan, K., Yang, J.: Secure
distributed programming with value-dependent types. In: Chakravarty, M.M.T.,
Hu, Z., Danvy, O. (eds.) Proceeding of the 16th ACM SIGPLAN international
conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 1921, 2011. pp. 266–278. ACM (2011)
29. Tofte, M.: Type inference for polymorphic references. Inf. Comput. 89(1), 1–34
(Sep 1990)
30. Wright, A.K.: Simple imperative polymorphism. In: LISP and Symbolic Computation. pp. 343–356 (1995)
31. Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput.
115(1), 38–94 (1994)
32. Xi, H.: Applied Type System (extended abstract). In: post-workshop Proceedings
of TYPES 2003. pp. 394–408. Springer-Verlag LNCS 3085 (2004)
33. Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings
of the 26th ACM SIGPLAN Symposium on Principles of Programming Languages.
pp. 214–227. San Antonio (January 1999)

