Pragmatic Gradual Polymorphism with References
Wenjia Ye and Bruno C. d. S. Oliveira
The University of Hong Kong, Hong Kong SAR, China{wjye,bruno}@cs.hku.hk

Abstract. Gradualizing System F has been widely discussed. A big challenge isto preserve relational parametricity and/or the gradual guarantee. Most past work
has focused on the preservation of parametricity, but often without the gradualguarantee. A few recent works satisfy both properties by giving up System F syntax, or with some restrictions and the introduction of sophisticated mechanisms
in the dynamic semantics.
While parametricity is important for polymorphic languages, most mainstream
languages typically do not satisfy it, for a variety of different reasons. In thispaper, we explore the design space of polymorphic languages that satisfy thegradual guarantee, but do not preserve parametricity. When parametricity is nota goal, the design of polymorphic gradual languages can be considerably simplified. Moreover, it becomes easy to add features that are of practical importance,such as mutable references. We present a new gradually typed polymorphic calculus, called λGgpr , with mutable references and with an easy proof of the gradualguarantee. In addition, compared to other gradual polymorphism work, λGgpr isdefined using a Type-Directed Operational Semantics (TDOS), which allows the
dynamic semantics to be defined directly instead of elaborating to a target castlanguage. λGgpr and all the proofs in this paper are formalized in Coq.
Keywords: Gradual Typing · Type System · Polymorphism.

1

Introduction

Statically typed languages can statically detect potential errors in programs, but mustnecessarily be conservative and reject some well-behaved programs. With dynamically
typed languages, all programs are accepted, which offers a great amount of flexibility.
However, the accepted dynamic programs include programs with type errors, making
it harder to detect programs that are ill-behaved because of type errors. Considering
the weaknesses and advantages of static and dynamic type systems, many approaches
have proposed to integrate these two spectrums [1, 7, 8, 22, 35]. Gradual typing [31, 35]
provides a smooth integration of the two styles and has been under active research inthe programming languages community. In addition to the type soundness property, agradual language should behave as a static language if it is fully annotated. Conversely,
it should behave as a dynamic language for fully dynamic programs. Importantly, thegradual guarantee [32] has been proposed to ensure a smooth transition between staticand dynamic typing.
The importance of System F as a foundation for programming languages with polymorphism naturally leads to the question of whether it is possible to gradualize it. Various researchers have explored this question. In this line of research, a long-standing goal

2

W. Ye, B. C. d. S. Oliveira

has been how to preserve relational parametricity [28]. Parametricity ensures a uniform
behavior for all instantiations of polymorphic functions, and is an important property of
System F. In addition it is also desirable to preserve the gradual guarantee [32], whichis recognized as an important property for gradual languages. Unlike System F, where
no dynamic mechanism is needed to ensure parametricity, with gradualized versions of
System F this is no longer the case. Ahmed et al. [3] showed that parametricity can be
enforced using a dynamic sealing mechanism at runtime. They prove parametricity, but
the gradual guarantee is not discussed. Igarashi et al. [17] improved on the dynamic
sealing approach and proposed a more efficient mechanism. While the gradual guarantee has been discussed, it was left as a conjecture. Toro et al. [37] even proved that
gradual guarantee and parametricity are incompatible. By giving up the traditional System F syntax, New et al. [24] proved the gradual guarantee and parametricity by using
user-provided sealing annotations, but this requires resorting to syntax that is not basedon System F. Finally, Labrada et al. [20] proved the gradual guarantee and parametricity
by inserting sealing with some restrictions. For instance, only base and variable types
can be used to instantiate type applications.
While parametricity is highly valued and it is guaranteed in practice in some functional languages, many mainstream programming languages – such as Java, TypeScript
or Flow – do not have parametricity. In mainstream languages the value of parametric polymorphism, and its ability to express a whole family of functions in a reusable
and type-safe manner is certainly recognized. However, such languages are imperativeand come with a variety of programming language features (such as unrestricted formsof mutable state, exceptions, parallelism and concurrency mechanisms, reflection, etc.)that make it hard to apply reasoning principles known in functional programming. In
particular, most of those features are known to be highly challenging to deal with in thepresence of parametricity [2, 18, 23]. This makes it non-obvious how to design a language with all those features, while preserving parametricity, in the first place. Moreover, preserving parametricity may require extra dynamic checks at runtime, which for
implementations where performance is a critical factor may discourage implementersfrom doing such checks. Therefore all the aforementioned programming languages support System F like mechanisms to deal with polymorphism and benefit from the reuseafforded by polymorphism. However, the reasoning principles that arise from polymorphism, such as parametricity is discarded, and parametricity is not enforced.
In particular, programming languages such as TypeScript or Flow, which support
some form of gradual/optional typing, and are widely used in practice, do not support
parametricity. Figure 1 encodes an example from Ahmed et al.’s work [3], which wasused to illustrate the parametricity challenge in gradual typing, in TypeScript and Flow.
In this program, the polymorphic function Ks has a polymorphic type: (X → Y → Y),
where X and Y are type variables. In a calculus with parametricity, we know that afunction with such type should always return the second argument or, in the presenceof runtime casts, return an error. In the program, Ks is as a function that casts a dynamic
constant function (K) that returns the first argument, which violates parametricity. When
the TypeScript and Flow programs are run the first argument 2 is returned, illustratingthat both languages do not enforce parametricity. In a gradual language with parametricity the result that we would expect is an error. Furthermore, even if we turn to TypedPragmatic Gradual Polymorphism with References
function K(x:any, y:any): any {return x;function K(x:any, y:any): any {return x;}}function Ks<X, Y>(x: X, y: Y): Y {let CAST = (K as any) as ((x:function Ks<X, Y>(x: X, y: Y): Y {let CAST = ((K : any) : ((x:X, y: Y) ⇒ Y);
return CAST(x, y);3

X, y: Y) ⇒ Y));return CAST(x, y);}}function run() {console.log(Ks<number,number>(2,3));function run() {console.log(Ks (2,3));}}(a) TypeScript code.

(b) Flow code.

Fig. 1: Ahmed et al. [3] program for illustrating parametricity in TypeScript and Flow.
Racket [36], which is a well-established gradual language used in both gradual typing
research and in practice, the result is similar and 2 is returned:(: K Any)(define K ( λ (x) ( λ (y) x)))(define Ks(cast K (All (X Y) (→ X (→ Y Y)))))((Ks 2) 3)

Therefore Typed Racket does not enforce parametricity either.
In this paper, we explore the more pragmatic design space of polymorphic graduallanguages with the gradual guarantee, but no parametricity. We believe that such designs are relevant because many practical language designs do not support parametricity, but support various other programming features instead. Dropping the requirement
for parametricity enables us to explore language designs with many relevant practical features, while being in line with current designs for existing practical gradually
typed languages. In particular, this paper studies the combination of parametric polymorphism, gradual typing and references. We show that, when parametricity is not agoal, the design of gradually polymorphic languages can be simplified, making it easier
to add features such as references. Moreover, the gradual guarantee, which has shown
to be quite problematic in all existing calculi with gradual polymorphism, is simple toachieve. We present a standard static calculus with polymorphism and mutable references called λgpr . Then we introduce the gradual counterpart, called λGgpr .
The approach that we follow to give the dynamic semantics to λGgpr is to use therecently proposed Type-Directed Operational Semantics TDOS [16, 42]. In contrast,
traditionally the semantics of a gradually typed language is defined by elaboration toa target cast calculus such as the blame calculus [39]. In other words, the dynamic
semantics of the gradual source language is given indirectly by translating to the target

4

W. Ye, B. C. d. S. Oliveira

language. As Ye et al. [42] shows, TDOS avoids such indirection and uses bidirectional
typing and type annotations to enforce both implicit and explicit casting at runtime in
gradually typed languages.
In summary, we make the following contributions in this paper:– The λGgpr calculus: A gradual calculus with polymorphism and mutable references.
λGgpr calculus is the gradual counterpart of the λgpr calculus. Both λGgpr and λgpr are
shown to be type sound and deterministic.
– Gradual guarantee for λGgpr . We prove the gradual guarantee for λGgpr . The proof
is easy and quite simple, in contrast to previous work in gradual polymorphism,
where the gradual guarantee was a major obstacle.
– A TDOS extension. TDOS has been applied to gradual typing before [42]. However, the previous work on TDOS for gradual typing only works in a purely functional, simply typed calculus. Our work shows that the TDOS approach can incorporate other features, including polymorphism and references.
– A mechanical formalization in the Coq theorem prover. All the calculi andproofs in this paper have been mechanically formalized in the Coq theorem prover.
The Coq formalization can be found in the supplementary materials of this paper:https://www.zenodo.org/badge/latestdoi/581421930

2

Overview

This section provides a background for gradual polymorphic calculi, calculi with gradual references and the key ideas of our static system (λgpr ) with polymorphism andreferences and its gradual counterpart (λGgpr ).
2.1

Background

Gradual References. Mutable references read or write content into a memory cell.
A common set of operations is: allocating a memory cell (ref e); updating references(e1 := e2 ) and reading the content from a reference (!e). Locations (o) point to thememory cell. For a reference value ref 1, a new location (o) is generated and value 1
is stored in the cell at the location o. If 2 is assigned to this location o := 2, the cellvalue is updated to 2. Later, when we read this cell (!o), 2 is returned. Siek et al. [31]defined an invariant consistency relation for reference types. Reference types are only
consistent with themselves. For example:(λx. (x := 2) : Ref ⋆ → Ref ⋆) (ref 1)– Rejected! Ref Int / Ref ⋆Although the type Int is consistent with ⋆, it does not mean that Ref Int is consistent
with Ref ⋆. Therefore, the argument type is not consistent with the function input, andthe program is rejected. Herman et al. [14] proposed a gradually typed lambda source
language with references, which defines the dynamic semantics by elaborating to a coercion calculus. The above program is allowed in their calculus. They define variant
consistency where if A is consistent with B then Ref A is consistent with Ref B. In theirPragmatic Gradual Polymorphism with References

5

calculus, casts are combined to achieve space-efficiency. Furthermore, Siek et al. [33]explored monotonic references with variant consistency. Their main consideration isspace efficiency. No runtime overhead is imposed in the statically typed part of programs. All the above works have not considered the gradual guarantee.
Toro and Tanter [38] showed how to employ the Abstracting Gradual Typing (AGT) [12]methodology to design a gradually typed calculus with mutable references (λREF
g ). Their
dynamic semantics of the source language is defined by translating to an evidence basecalculus. They prove a bisimulation with the coercion calculus by Herman et al. [14].
λREF
g is proved to satisfy the gradual guarantee. The consistency of λREF
g is also variant.
Gradual Polymorphism. Gradual polymorphism is a popular topic. Researchers havebeen working in this area for a long time. Prior work has focused on two key properties:
relational parametricity [28] and the gradual guarantee [32]. Relational parametricity
ensures that all instantiations to a polymorphic value behave uniformly. The gradualguarantee ensures that less dynamic programs behave the same as more static programs.
Satisfying these two properties at once has shown to be problematic. Ahmed etal. [3] showed that a naive combination of the unknown type ⋆ and type substitution
breaks relational parametricity. They show the problem using a simple expression withtwo casts. To simplify the presentation, we ignore blame labels. Suppose that K ⋆ =⌈λx.λy.x⌉, the dynamically typed constant function, is cast to a polymorphic type:K ⋆ : ⋆ ⇒ ∀X. ∀Y. X → Y → X

K ⋆ : ⋆ ⇒ ∀X. ∀Y. X → Y → Y

The notation e : A ⇒ B, borrowed from the blame calculus [29], means cast expression e from type A to type B. The constant function K ⋆ returns the first argument.
Considering relational parametricity, a value of type ∀X. ∀Y. X → Y → X should
be a constant value which always returns the first argument. While a value of type
∀X. ∀Y. X → Y → Y should return the second argument. Therefore, the first cast succeeds and the second cast should fail. However, if these two casts are applied to thearguments in the usual way employing type substitutions, then we obtain the following:(K ⋆ : ⋆ ⇒ ∀X. ∀Y. X → Y → X) Int Int 2 3,→∗ (K ⋆ : ⋆ ⇒ Int → Int → Int),→∗ 2
(K ⋆ : ⋆ ⇒ ∀X. ∀Y. X → Y → Y) Int Int 2 3,→∗ (K ⋆ : ⋆ ⇒ Int → Int → Int),→∗ 2
The second cast succeeds and returns the first argument, which breaks parametricity.
The reason for this behavior is that, after the type substitution, the polymorphic information is lost. Note that, as we have seen in Section 1, this is exactly how various
practical languages (TypeScript, Flow and Typed Racket) behave.
Much of the work on gradual polymorphism aims at addressing the above problem. That is, for the second cast we would like to obtain blame instead of 2, so thatparametricity is not violated. While the preservation of parametricity is a worthy goal,6

W. Ye, B. C. d. S. Oliveira

it typically requires substantial changes to a calculus to ensure its preservation, sincenaive direct type substitutions do not work. Furthermore this also affects proofs, which
can become significantly more complicated due to the changes in the calculus. To address this problem a well-known approach, originally proposed by Ahmed et al. [3], is toemploy dynamic sealing. With dynamic sealing we do not do the substitution directly
but record a fresh variable binding. However, even calculi that satisfy parametricity
have to compromise on the important gradual guarantee property, or System F syntax,
or be equiped with heavy forms of runtime evidence [20, 37]. A thorough discussion ofvarious approaches is given in Section 6.
2.2

Key Ideas

Our key design decision is to give up support for parametricity in exchange for a simpler
calculus that is also easier to extend with other important practical features. In particular, in our work we illustrate how to obtain a polymorphic gradually typed calculus,
with gradual references and with the gradual guarantee. In contrast, none of the existing gradually polymorphic calculi supports references and the gradual guarantee is only
supported with restrictions [20]; or major modifications in the syntax and semantics ofthe language [24]; or not supported/proved at all [3, 17, 37].
A direct semantics with a TDOS. Our gradually typed calculus λGgpr has a direct semantics by using a (TDOS) [15] approach. In λGgpr , type annotations are operationally relevant and they basically play a role similar to casts. Nevertheless, implicit casts should
also be enforced for a gradual calculus at runtime. Most previous work makes the implicit casts explicit via the elaboration process. That is the reason why dynamic semantics is not defined directly. We resort to bidirectional typing with inferred (⇒) andchecked (⇐) modes. Using the checking mode of bidirectional typing, the consistency(∼) between values and the checked type is checked and enforced via an implicit cast.
At compile time, the flexible consistency relation allows more programs to be accepted,
while the checking mode signals casts that are needed at runtime. For example, in thetyping rule for applications.
Σ; Γ ⊢ e1 ⇒ A1 → A2

Σ; Γ ⊢ e2 ⇐ A1

Σ; Γ ⊢ e1 e2 ⇒ A2

Typ-app

The checking mode signals an implicit cast for the argument. The argument e2 is checked
to be consistent with the type A1 using the bidirectional subsumption rule:Σ; Γ ⊢ e ⇒ BΓ⊢B∼AΣ; Γ ⊢ e ⇐ A

Typ-sim

For instance, (λx. x : Int → Int) (True : ⋆) type-checks, but at run-time the invalid castto the value argument (True : ⋆) is detected and an error is reported.
Conservativity, no parametricity and direct substitutions. The λGgpr calculus is a conservative extension of its static counterpart. Notably, our λGgpr is a simple polymorphic

Pragmatic Gradual Polymorphism with References

7

calculus, without using mechanisms such as dynamic sealing and evidences. Instead,since parametricity is not a goal, we can simply use direct type substitutions during
reduction as follows:((ΛX. e : A) : ∀X. B) C ,→ e[X 7→ C] : A[X 7→ C] : B[X 7→ C]
Our type application rule substitutes type directly unlike in previous work with dynamic
sealing where a fresh type name variable is generated and stored in a global or local
context. Dynamic sealing takes extra time and space. With a large enough number oftype applications, the space consumption may go unbounded.
Gradual guarantee and references. Furthermore, λGgpr is mechanically formalized andshown to have the gradual guarantee. Our application of the eager semantics and the
choice of value forms for λGgpr simplify the gradual guarantee. To prove the gradualguarantee we need a precision (⊑) relation. The gradual guarantee theorem needs toensure that if the more static program does not go wrong, then the less static program
should not go wrong as well. The precision relation is used to relate two programs,
which have different type information. Type precision compares the amount of static
type information for programs and types. A type is more precise than another if it ismore static. The unknown type (⋆) is the least precise type, since we do not have any
static information about that type. Let’s consider two programs:
λx. 1 : Int → Int
λx. 1 : ⋆ → ⋆The first one is more precise than the second one because the second program is fully
dynamic. The value forms of λGgpr are annotated and include terms such as i : Int and(λx. e : A → B) : C. The simplicity of the proof of the gradual guarantee is greatly
related to the choice of representation of values. In λGgpr , the gradual guarantee theorem
can be formalized in a simple way with a lemma similar to a lemma proposed by Garcia
et al. [12]. The lemma states that if e1 is more precise than e2 and e1 takes a step to e′1then e2 takes a step to e′2 and e′1 is more precise than e′2 . With this lemma, we can inferthat two expressions related by precision have the same behavior. Thus, this lemma isenough to obtain the dynamic gradual guarantee. Notably, λGgpr is extended with mutable references using a form of variant consistency [14, 38]. This is in contrast to thepreviously discussed gradually polymorphic calculi where references are not supported.

3

The λ g pr Calculus: Syntax, Typing and Semantics

In this section, we will introduce the λgpr calculus, which is a calculus with references
and polymorphism. λgpr calculus is an extended version of System F with references andis the static calculus that serves as a foundation for the gradual calculus in Section 4.
3.1

SyntaxThe syntax of the λgpr calculus is shown in Figure 2.

8

W. Ye, B. C. d. S. Oliveira

SyntaxTypes
Expressions
ValuesContexts
StoresLocations
Frame

A, B F Int | A → B | X | ∀X. A | Unit | Ref A
e F x | i | λx : A. e | e : A | e1 e2 | ΛX. e | e A |!e | e1 := e2 | ref e | unit | ov F i | ΛX. e | λx : A. e | unit | oΓ F · | Γ, x : A | Γ, X
µ F · | µ, o = v
Σ F · | Σ, o : A
F F v □ | □ e | □ A |! □ | v1 := □ | □ := e2 | ref □ | □ : A

Fig. 2: λgpr syntax
Types. Meta-variables A, B range over types. Types include base types (Int), function
types (A → B), type variables (X), polymorphic types (∀X. A), the unit type Unit andreference types Ref A, which denotes a reference with type A.
Expressions. Meta-variables e range over expressions. Most of the expressions are
standard: variables (x), integers (i), annotations (e : A), applications (e1 e2 ), type applications (e A), dereferences (!e), assignments e1 := e2 , references (ref e), unit (unit),
locations o, lambda abstractions (λx : A. e) (which are annotated with input type A),
and type abstractions (ΛX. e).
Values. Meta-variables v range over values. A raw value is either an integer (i), a typeabstraction (ΛX. e), a lambda abstraction (λx : A. e), a unit (unit) or a location (o).
Contexts, stores, locations and frames. The type context Γ tracks the bound variables
x with their types and the bound type variables X. Typing location Σ tracks the boundlocations o with their types, while the store µ tracks locations with their stored values during the reduction process. Frames (F) include applications, type applications,dereferences, assignments and references.
3.2

Type System

Before introducing the type system, we show the well-formedness of types at the top of
Figure 3. The well-formedness of types ensures that there are no free type variables andthat each type variable is bound in the contexts.
Typing relation. The typing relation of λgpr is shown at the bottom of Figure 3. The typesystem essentially includes the usual System F rules, except that they also propagate thelocation typing context (Σ). Reference locations o are stored in the location typing context Σ (rule styp-loc). The bound type of locations indicates the type of stored values.
For instance, o points to 1 stored in a memory cell. The integer type for 1 is tracked by
the location o in the location typing context Σ. Other rules related to references such as
assignments (rule styp-assign), references (rule styp-ref) and dereferences (rule stypderef) are standard. Annotation expressions (e : A) are not necessary for the static

Pragmatic Gradual Polymorphism with ReferencesΓ⊢A

9(Well-formedness of types)

TW-intTW-unitTW-varX∈ΓΓ ⊢ IntΓ ⊢ UnitΓ⊢X

TW-arr
Γ⊢A

Γ⊢B

Γ⊢A→B

Σ; Γ ⊢ s e : A

TW-allΓ, X ⊢ A

TW-refΓ⊢AΓ ⊢ ∀X. AΓ ⊢ Ref A(Typing rules for expressions)STyp-lit

STyp-unit

STyp-var
x:A ∈ ΓSTyp-loco:A ∈ ΣΣ; Γ ⊢ s i : Int

Σ; Γ ⊢ s unit : Unit

Σ; Γ ⊢ s x : A

Σ; Γ ⊢ s o : Ref A

STyp-refΣ; Γ ⊢ s e : A
Σ; Γ ⊢ s ref e : Ref A
STyp-abs
Σ; Γ, x : A ⊢ s e : B
Σ; Γ ⊢ s λx : A. e : A → B

STyp-deref
Σ; Γ ⊢ s e : Ref A

STyp-assign
Σ; Γ ⊢ s e1 : Ref A
Σ; Γ ⊢ s e2 : A

Σ; Γ ⊢ s !e : A

Σ; Γ ⊢ s e1 := e2 : Unit

STyp-app
Σ; Γ ⊢ s e1 : A1 → A2
Σ; Γ ⊢ s e2 : A1

STyp-anno
Σ; Γ ⊢ s e : A

Σ; Γ ⊢ s e1 e2 : A2

Σ; Γ ⊢ s (e : A) : A

STyp-tabs
Σ; Γ, X ⊢ s e : A

STyp-tappΓ⊢AΣ; Γ ⊢ s e : ∀X. B

Σ; Γ ⊢ s ΛX. e : ∀X. A

Σ; Γ ⊢ s e A : B[X 7→ A]

Fig. 3: The type system of λgpr calculus.
system where the annotated types are syntactically equal (rule styp-anno), but they willplay an important role in the gradual system and are included here.
Definition 1 defines well-formed stores (µ) with respect to the typing locations Σ, using
the typing relation:
Definition 1 (Well-formedness of the store with respect to Σ).
Σ ⊢ µ ≡ i f dom(µ) = dom(Σ) and Σ; · ⊢ µ(o) : Σ(o), f or every o ∈ µ
A store is well-formed with the typing location if the store and the typing location
contain the same domains. For each location, which is in the store, the bounded valueµ(o) can be inferred with the type bound in the typing location (Σ(o)).
3.3Dynamic Semantics

The operational semantics for the λgpr calculus is shown in Figure 4 (we ignore thegray parts for now). µ; e ,→ µ′ ; e′ represents the reduction rules, which states that ewith store µ reduces to e′ with the updated store µ′ . The reduction rules of λgpr are

10

W. Ye, B. C. d. S. Oliveiraµ; e ,→ s µ′ ; e′(Operational semantics)

step-evalµ; e ,→ s µ′ ; e′µ; F[e] ,→ s µ ; F[e ]′′step-annov

step-assignµ; v : A : A ,→ s µ; v : Aµ; o := v ,→ s µ[o 7→ v]; unit

step-tap

step-derefo=v ∈ µµ; ((ΛX. e) : ∀X. A ) A ,→ s µ; (e[X 7→ A]) : (A[X 7→ A])µ; !o ,→ s µ; v : A

step-beta

step-refvo<µµ; ((λx : A. e) : A → B ) v ,→ s µ; e[x 7→ v] : B : Bµ; ref v ,→ s µ, o = v; oFig. 4: Reduction rules for λgpr .
straightforward. A reference value is bound in the store by a fresh location as shownin rule step-refv. The dereference rule extracts the bound value of the location in thestore (rule step-deref). Rule step-eval evaluates the frames. Let’s see how the example
o1 := (ΛX. (λx : X. x) !o2 ) Int with the existing store o1 = 1, o2 = 2 reduces. 2 isread from store o1 = 1, o2 = 2. After the type substitution, 2 is substituted into thelambda. Then 2 is used to update the store pointed by o1 . Finally, the store becomes
o1 = 2, o2 = 2. The detailed steps are as follows:
o1 = 1, o2 = 2; o1 := (ΛX. (λx : X. x) !o2 ) Int,→ {by rule Step-eval, rule Step-deref }o1 = 1, o2 = 2; o1 := (ΛX. (λx : X. x) 2) Int,→ {by rule Step-tap }o1 = 1, o2 = 2; o1 := (λx : Int. x) 2,→ {by rule Step-beta}
o1 = 1, o2 = 2; o1 := 2,→ {by rule Step-assign}
o1 = 2, o2 = 2; unit
Theorem 1 shows that the λgpr calculus is deterministic:
Theorem 1 (Determinism of λgpr ). If Σ; · ⊢ s e : A, Σ ⊢ µ, µ; e ,→ s µ1 ; e1 and µ; e ,→ s
µ2 ; e2 then e1 = e2 and µ1 = µ2 .
Furthermore, the preservation Theorem 2 and progress Theorem 3 of λgpr calculus areshown below:
Theorem 2 (Type Preservation of λgpr ). If Σ; · ⊢ s e : A, Σ ⊢ µ and µ; e ,→ s µ′ ; e′ thenΣ ′ ; · ⊢ s e′ : A, Σ ′ ⊢ µ′ and Σ ′ ⊇ Σ.
Theorem 3 (Progress of λgpr ). If Σ; · ⊢ s e : A then e is a value or ∃e′ µ′ , µ; e ,→ s µ′ ; e′ .

Pragmatic Gradual Polymorphism with References

11⇔ F ⇒|⇐

Typing modes

Σ; Γ ⊨ s e ⇔ A(Typing rules for expressions)sty-litsty-unit

sty-varx:A ∈ Γsty-loc
o:A ∈ ΣΣ; Γ ⊨ s i ⇒ Int

Σ; Γ ⊨ s unit ⇒ Unit

Σ; Γ ⊨ s x ⇒ AΣ; Γ ⊨ s o ⇒ Ref A

sty-deref
Σ; Γ ⊨ s e ⇒ Ref A

sty-assign
Σ; Γ ⊨ s e1 ⇒ Ref A
Σ; Γ ⊨ s e2 ⇐ A

Σ; Γ ⊨ s ref e ⇒ Ref A

Σ; Γ ⊨ s !e ⇒ AΣ; Γ ⊨ s e1 := e2 ⇒ Unit

sty-abs
Σ; Γ, x : A ⊨ s e ⇒ B

sty-appΣ; Γ ⊨ s e1 ⇒ A1 → A2
Σ; Γ ⊨ s e2 ⇐ A1

sty-anno
Σ; Γ ⊨ s e ⇐ AΣ; Γ ⊨ s e1 e2 ⇒ A2

Σ; Γ ⊨ s e : A ⇒ A

sty-ref
Σ; Γ ⊨ s e ⇒ AΣ; Γ ⊨ s λx : A. e ⇒ A → B

sty-tappsty-eqΣ; Γ ⊨ s e ⇒ A

sty-tabs
Σ; Γ, X ⊨ s e ⇒ AΓ⊢AΣ; Γ ⊨ s e ⇒ ∀X. B

Σ; Γ ⊨ s e ⇐ AΣ; Γ ⊨ s ΛX. e ⇒ ∀X. A

Σ; Γ ⊨ s e A ⇒ B[X 7→ A]

Fig. 5: Bidirectional typing for the λgpr calculus.
3.4

Bidirectional Typing

We also present a set of bidirectional typing rules (shown in Figure 5) for λgpr . Althoughbidirectional typing is not essential for λgpr , it is used later for the gradual typing criteria
proofs. The typing judgment is represented as Σ; Γ ⊢ e ⇔ A. The expression e isinferred (⇒) or checked (⇐) by type A under the typing context Γ and location typing
context Σ. Typing modes (⇔) contain the inference mode (⇒) and checking mode (⇐),
which are shown at the top of Figure 5. One extra rule is rule sty-eq, which switches
modes. We proved that the two type systems are equivalent:Lemma 1 (Typing Equivalence for λgpr ). Σ; Γ ⊢ s e : A iff Σ; Γ ⊨ s e ⇔ A.

4

The λGgpr Calculus

This section introduces the λGgpr calculus, which gradualizes the λgpr calculus. Normally,a gradually typed lambda calculus (GTLC) does not define the operational semantics
directly, but is elaborated to a cast calculus. λGgpr instead defines the dynamic semantics
directly using the TDOS approach [15]. λGgpr is proved to be type sound and it has a
gradual guarantee. The calculus does not have parametricity, enabling simplifications

12

W. Ye, B. C. d. S. Oliveira

SyntaxTypes
Expressions
Results
Raw Values
ValuesContexts
StoresLocation
Frame

A, B F Int | A → B | X | ∀X. A | Unit | Ref A | ⋆e F x | i | e : A | e1 e2 | e A |!e | e1 := e2 | ref e | unit | o | ΛX. e : A | λx. e : A → B
r F e | blameu F i | ΛX. e : A | λx. e : A → B | unit | ovFu:AΓ F · | Γ, x : A | Γ, X
µ F · | µ, o = v
Σ F · | Σ, o : A
F F v □ | □ e | □ A |!□ | v1 := □ | □ := e2 | ref □Γ⊢A∼B(Consistency)

S-unit

S-var
Γ⊢X

S-z

S-dynlΓ⊢A

S-dynrΓ⊢AΓ ⊢ Unit ∼ UnitΓ⊢X∼XΓ ⊢ Int ∼ Int

Γ⊢⋆∼A

Γ⊢A∼⋆

S-arr

Γ ⊢ A1 ∼ B1
Γ ⊢ A2 ∼ B2

S-forallΓ, X ⊢ A ∼ B

S-ref
Γ⊢A∼B

Γ ⊢ A1 → A2 ∼ B1 → B2Γ ⊢ ∀X. A ∼ ∀X. B

Γ ⊢ Ref A ∼ Ref B

Fig. 6: λGgpr syntax and consistency.
in the calculus, and the addition of features such as gradual references, which none ofthe previous gradual calculi with polymorphism support.
4.1

Static Semantics

Syntax, type well-formedness and consistency. Figure 6 shows the syntax and consistency of the λGgpr calculus. The gray parts are the same as λgpr . The λGgpr calculus extends
types with the unknown type ⋆ with respect to λgpr . Because of the power of the unknown type ⋆, dynamic type checking is required and run-time errors may be raised.
Therefore, in addition to expressions, λGgpr has the run-time error blame. Because of
the run-time checking requirement for the gradual typing system, we need annotations
for type abstractions and lambda abstractions. Furthermore, due to the imprecision of
the unknown type ⋆, values are also annotated. Otherwise, examples such as 1 : ⋆ aretroublesome. Because of the value forms, annotations are not included in frames, unlikein the λgpr calculus. We will explain the details later.
Well-formed types are extended with the following rule for the unknown type ⋆:Γ⊢⋆Notably, instead of syntactic equality, a more general relation called consistency (Γ ⊢A ∼ B) is defined in λGgpr . Every well-formed type is consistent with itself. The unknownPragmatic Gradual Polymorphism with References
Σ; Γ ⊢ e ⇔ A

13(Typing rules for expressions)Typ-litTyp-unit

Typ-varx:A ∈ ΓTyp-loc
o:A ∈ ΣΣ; Γ ⊢ i ⇒ Int

Σ; Γ ⊢ unit ⇒ Unit

Σ; Γ ⊢ x ⇒ AΣ; Γ ⊢ o ⇒ Ref A

Typ-ref
Σ; Γ ⊢ e ⇒ A

Typ-deref
A1 ▷ Ref A
Σ; Γ ⊢ e ⇒ A1

Typ-assign
A1 ▷ Ref A
Σ; Γ ⊢ e1 ⇒ A1
Σ; Γ ⊢ e2 ⇐ A

Σ; Γ ⊢ ref e ⇒ Ref A

Σ; Γ ⊢!e ⇒ AΣ; Γ ⊢ e1 := e2 ⇒ Unit

Typ-abs
Σ; Γ, x : A ⊢ e ⇐ B

Typ-appA ▷ A1 → A2
Σ; Γ ⊢ e1 ⇒ A
Σ; Γ ⊢ e2 ⇐ A1

Typ-anno
Σ; Γ ⊢ e ⇐ AΣ; Γ ⊢ λx. e : A → B ⇒ A → B

Σ; Γ ⊢ e1 e2 ⇒ A2

Σ; Γ ⊢ e : A ⇒ A

Typ-simΓ⊢A∼B
Σ; Γ ⊢ e ⇒ A

Typ-tabs
Σ; Γ, X ⊢ e ⇐ A

Typ-tappΓ⊢AΣ; Γ ⊢ e ⇒ A1
A1 ▷ ∀X. B

Σ; Γ ⊢ e ⇐ BΣ; Γ ⊢ ΛX. e : A ⇒ ∀X. A

Σ; Γ ⊢ e A ⇒ B[X 7→ A]

A ▷ A1 → A2

A ▷ ∀X. A1

A ▷ Ref A1

A→B▷A→B∀X. A ▷ ∀X. A

Ref A ▷ Ref A⋆▷⋆→⋆⋆ ▷ ∀X. ⋆⋆ ▷ Ref ⋆Fig. 7: The type system for the λGgpr calculus.
type is consistent with any other well-formed type. Structural types such as functions,references and polymorphic types are consistent if their type sub-components are consistent. Note that for two reference types, consistency is variant: if A and B are consistent then Ref A and Ref B are consistent. Unlike invariant consistency [31], type A and
B do not have to be the same. As usual, consistency is reflexive and symmetric, but nottransitive. We use the following abbreviation for consistency: A ∼ B ≡ · ⊢ A ∼ B.
Typing relation. Bidirectional typing is used to design the type system. Bidirectional
typing is not essential for λgpr but it is necessary for λGgpr . Annotation expressions (e : A)
and the checking mode (⇐) signal the use of casts (explicitly or implicitly) at run-time.
The typing rules of the λGgpr calculus are shown in Figure 7. They are almost the sameas λgpr ’s type system. For rule Typ-app, rule Typ-tapp, rule Typ-assign and rule Typderef, the unknown type ⋆ can be matched with, respectively, a dynamic function type(⋆ → ⋆), a dynamic polymorphic type (∀X. ⋆) and a dynamic reference type (Ref ⋆).
In a system with gradual typing and the unknown type ⋆ we always have to consider

14

W. Ye, B. C. d. S. Oliveiracases where the type may be unknown. For instance in an application e1 e2 , e1 caninfer a function type as usual, but it can also infer type ⋆ and still be well-typed. So, amatching function (A ▷ B) is needed to account for both possibilities. The table at thebottom of Figure 7 shows the definition of the matching functions A ▷ B. Note that weoverload the notation, but there are 3 different matching functions, in each column of
the table, that are employed by the rules correspondingly. For example, rule Typ-deref
employs the matching function in the third column of the table. The first row in the table
depicts the form of the matching function, while the other two rows give its definition.
The checking mode rule Typ-sim is generalized to check if the inferred type A andchecked type B are consistent. Note that rule Typ-sim is the only rule in the checkedmode and, as such, does not overlap with anything else. Moreover, all the rules in theinference mode are syntax directed. Therefore, the rules are basically directly implementable, as usual for bidirectional type-checking rules. Note that in λGgpr annotation
expressions combined with consistency play an important role, where more programs
are allowed. For instance, (λx. ((x : ⋆) 1) : Bool → ⋆) True is accepted, but raises a
blame error at run-time. Note that dynamically typed lambdas λx.e are syntactic sugarfor λx.e : ⋆ → ⋆. The use of this syntactic sugar enables us to encode the dynamically
typed lambda calculus (DTLC) [4] easily in λGgpr .
Definition 2 shows dynamic type checking for raw and annotated values, which
is done at run-time. Dynamic type checking for values exploits the annotations thatare present at run-time, and does not make use of the typing relation. Dynamic typechecking is essentially a constant time operation, with little cost (note that the function
is not recursive).
Definition 2 (Dynamic type). |u|µ = A and |v|µ = A denote the dynamic type of the raw
and annotated values.
|i|µ = Int|(λx. e : A → B)|µ = A → B|(ΛX. e : A)|µ = ∀X. A|unit|µ = Unit|o|µ = Ref |v|µwhen o = v ∈ µ|(u : A)|µ = A|u|µ = A states that the dynamic type of the raw value u is A under store µ. Notably,
for locations o, the dynamic type is defined by the dynamic type of the bounded values
in the store. Other rules are straightforward. Lemma 2 shows that if a raw value can beinferred with type A, then its dynamic type is type A as well.
Lemma 2 (Synthesis of Dynamic Types). For any raw value u, if Σ ⊢ µ and Σ; · ⊢u ⇒ A then |u|µ = A.
As in λgpr , a term typed using the inference mode is guaranteed to infer a unique
type. In addition, Lemma 3 shows that each well-typed term can be checked.
Lemma 3 (Synthesis principality). If Σ; Γ ⊢ e ⇒ A then exists B, Σ; Γ ⊢ e ⇐ B andΓ ⊢ A ∼ B.

Pragmatic Gradual Polymorphism with Referencesµ; v ,→A µ′ ; r

15(Casting for values)
casting-sim|u|µ ∼ B

casting-nsim¬|u|µ ∼ Bµ; u : A ,→B µ; u : Bµ; u : A ,→B µ; blameµ; v ,→B,A µ′ ; r(Double casting)

TLists-basebµ; v ,→A µ; blame

TLists-consµ; v ,→A µ; v′µ; v′ ,→B µ; rµ; v ,→B,A µ; blameµ; v ,→B,A µ; r

Fig. 8: Casting for values
4.2

Dynamic Semantics

The dynamic semantics contains two parts. The first part is casting, which casts a value
to another value with a target type. In casting the dynamic type of the value is the source
type. The second part is the reduction rules.
Casting. Figure 8 shows the casting rules of the λGgpr calculus. µ; v ,→A µ; r represents casting values v by type A under store µ. The dynamic type of the raw values
u is checked to be consistent with type A or not. If two types are consistent, then theintermediate type can be removed and the raw values are annotated with target types.
Otherwise, a run-time error is raised. For example when 1 : ⋆ is cast by type Bool, thedynamic type of 1 is Int, which is not consistent with Bool, and blame is raised. While in
1 : ⋆ cast by type Int, the type Int is consistent with type Int. Thus, type ⋆ is erased and1 is annotated with type Int. Since a location o is a raw value, if we want to obtain the
dynamic type of the location, we should obtain it from the store µ. Therefore, castinguses the store. Casting by two types is shown at the bottom of Figure 8. It simply casts
the types one by one, using the basic casting relation.
Reduction. The reduction rules of λGgpr calculus are shown in Figure 9. Raw values
are reduced to become values, which are annotated by the dynamic type of the raw
values with rule step-u. Due to this rule, annotations are not included in the frame. Annotated expressions are further dealt by rule step-anno and rule step-annop. From thetyping rules of rules Typ-app, Typ-tapp, Typ-assign, and Typ-deref, type ⋆ is allowed
to match, respectively, a dynamic function, a polymorphic function or a reference type.
Moreover, we know that ⋆ is consistent with any type. Therefore, we should check
whether the internal values cannot match with the wanted type structure. For example,
ill-formed applications ((1 : ⋆) 2) where the internal value (1) is not an lambda abstraction. There are similar examples for type applications and assignments: (1 : ⋆) Booland (True : ⋆) := 2 where 1 is not a type abstraction and True is not a location. Using

16

W. Ye, B. C. d. S. Oliveiraµ; e ,→ µ′ ; r(Operational semantics)

vstep-evalµ; e ,→ µ′ ; e′vstep-blameµ; e ,→ µ′ ; blame

vstep-annopµ; e ,→ µ′ ; blameµ; F[e] ,→ µ′ ; F[e′ ]µ; F[e] ,→ µ′ ; blameµ; e : A ,→ µ′ ; blame

vstep-beta
A ▷ A2 → B2µ; v ,→A1 ,A2 µ; v′

vstep-assigndµ; v1 ,→Ref ⋆ µ; blameµ; ((λx. e : A1 → B1 ) : A) v ,→ µ; e[x 7→ v′ ] : B1 : B2µ; v1 := v2 ,→ µ; blame

vstep-betap
vstep-annovµ; v ,→A µ; r

A ▷ A2 → B2µ; v ,→A1 ,A2 µ; blame

vstep-betadµ; v1 ,→⋆→⋆ µ; blameµ; v : A ,→ µ; rµ; ((λx. e : A1 → B1 ) : A) v ,→ µ; blameµ; v1 v2 ,→ µ; blame

vstep-tap
B ▷ ∀X. B2

vstep-tapdµ; v ,→∀X. ⋆ µ; blameµ; ((ΛX. e : A) : B) C ,→ µ; e[X 7→ C] : A[X 7→ C] : B2 [X 7→ C]µ; v B ,→ µ; blame

vstep-refvo<µvstep-derefo=v ∈ µµ; ref v ,→ µ, o = v; oA1 ▷ Ref A

vstep-derefpµ; v ,→Ref ⋆ µ; blameµ; !(o : A1 ) ,→ µ; v : Aµ; !v ,→ µ; blame

vstep-assign|o|µ = A1
A ▷ Ref A2µ; v2 ,→A1 ,A2 µ; v′2

vstep-assignp|o|µ = A1
A ▷ Ref A2µ; v2 ,→A1 ,A2 µ; blame

vstep-u|u|µ = Aµ; (o : A) := v2 ,→ µ[o 7→ v′2 ]; unitµ; (o : A) := v2 ,→ µ; blameµ; u ,→ µ; u : A

vstep-anno¬value e : Aµ; e ,→ µ′ ; e′µ; e : A ,→ µ′ ; e′ : A

Fig. 9: Reduction rules for λGgpr .

rules vstep-betad, vstep-tapd, vstep-derefp, and vstep-assignd, we cast the value tothe corresponding dynamic types and filter out programs with errors. To apply a value
to a functional value (rules vstep-beta and vstep-betap), the argument type must be
consistent with function input types A2 . Moreover, the expected substituted value typeis A1 . Thus, the argument value should be cast by A2 and A1 , which may return a blame
error. To preserve the type, the substituted body is annotated with B1 and B2 . When avalue v is annotated with a type A, the type of the value must be consistent with type A,
and run-time checking is needed to validate consistency (rule vstep-annov). A reference
value ref v is bound in the store with a fresh location o (rule vstep-refv). To obtain avalue from the store by the location, from the last expression we use rule vstep-deref.

Pragmatic Gradual Polymorphism with References

17

Note that in the typing rule for references:Σ; · ⊢ o : A1 ⇒ A1

A1 ▷ Ref A

Σ; · ⊢!(o : A1 ) ⇒ A

Typ-deref

The expected type is A but the bound value type is consistent with A. Thus we annotate
v using type A. When assigning a value to replace the bound value in the reference using
rules vstep-assign and vstep-assignp :Σ; · ⊢ o : A ⇒ A

A ▷ Ref A2

Σ; · ⊢ v2 ⇐ A

Σ; · ⊢ (o : A) := v2 ⇒ Unit

Typ-assign

The bound value by location o has type A1 , while the type of v2 is consistent with typeA2 and A2 is consistent with A1 . The expected type to be replaced is type A1 , therefore
v2 is cast by type A1 and A2 . Note that the cast result can be blamed. If a type is applied
to a polymorphic value, from the last expression (rule vstep-tap):B ▷ ∀X. B2

Σ; · ⊢ (ΛX. e : A) : B ⇒ BΣ; · ⊢ ((ΛX. e : A) : B) C ⇒ B2 [X 7→ C]

Typ-tapp

The expected type is (B2 [X 7→ C]) but the substituted expression (e[X 7→ C] : A[X 7→C]) has type (A[X 7→ C]), so it is annotated with type (B2 [X 7→ C]).
Properties of λGgpr . λGgpr is deterministic (Theorem 4) and type sound (Theorem 5 andTheorem 6).
Theorem 4 (Determinism of λGgpr ). If Σ; · ⊢ e ⇔ A, µ; e ,→ µ1 ; r1 and µ; e ,→ µ2 ; r2then r1 = r2 and µ1 = µ2 .
Theorem 5 (Type Preservation of λGgpr ). If Σ; · ⊢ e ⇔ A, Σ ⊢ µ, and µ; e ,→ µ′ ; e′then Σ ′ ; · ⊢ e′ ⇔ A, Σ ′ ⊢ µ′ and Σ ′ ⊇ Σ.
Theorem 6 (Progress of λGgpr ). If Σ; · ⊢ e ⇔ A then e is a value or ∃r µ′ , µ; e ,→ µ′ ; r.

4.3

Gradual Typing Criteria

Siek et al. [31,32] proposed a set of criteria for gradual typing system. At the end of thespectrum, a fully annotated gradually typed program should behave as a statically typed
program. Conversely, a gradually typed program without annotations should behave asa dynamic program. Siek et al. proposed the gradual guarantee, which states that having
annotations that are more/less precise should not change the behavior of the programs.
Here we show that λGgpr has the gradual guarantee.
To prove the gradual guarantee, we define the precision for types, expressions andstores. At the top of Figure 10 is type precision A ⊑ B, which states that type A is
more precise than B. The unknown type ⋆ is less precise than any other types. Each
type is more precise than itself. The precision of functions, polymorphic functions and18

W. Ye, B. C. d. S. Oliveira

A⊑B(Type Precision)

tp-unittp-vartp-z

tp-dyntp-arrA1 ⊑ B1

Unit ⊑ Unit

X⊑XInt ⊑ IntA⊑⋆

A1 → A2 ⊑ B1 → B2

tp-forallA⊑B

tp-refA⊑B∀X. A ⊑ ∀X. B

Ref A ⊑ Ref B

e1 ⊑ e2A2 ⊑ B2(Expression Precision)

ep-litep-varep-unit

ep-o

ep-refe1 ⊑ e2

ep-derefe1 ⊑ e2i⊑ix⊑xunit ⊑ unito⊑oref e1 ⊑ ref e2!e1 ⊑!e2

ep-abse1 ⊑ e2A1 ⊑ A2
B1 ⊑ B2

ep-appe1 ⊑ e3

λx. e1 : A1 → B1 ⊑ λx. e2 : A2 → B2
ep-annoe1 ⊑ e2A1 ⊑ A2

ep-assign
e1 ⊑ e3e2 ⊑ e4

e1 e2 ⊑ e3 e4

ep-tabse1 ⊑ e2

e1 := e2 ⊑ e3 := e4ep-tappe1 ⊑ e2A1 ⊑ A2

ΛX. e1 : A1 ⊑ ΛX. e2 : A2

e1 : A1 ⊑ e2 : A2e2 ⊑ e4

A1 ⊑ A2

e1 A1 ⊑ e2 A2µ1 ⊑ µ2(Store Precision)
sp-nilsp-emptyµ1 ⊑ µ2·⊑·µ1 , o = v1 ⊑ µ2 , o = v2

v1 ⊑ v2

Fig. 10: Precision Relation.
reference types holds, if the precision of their sub-components holds. Note that the
precision of function types is ”covariant” in the argument types since to compare theprecision of the two programs:
λx. 1 : Int → Int
λx. 1 : ⋆ → Int
we should just say that the first one is more precise than the second one because theinput type of the second one is fully dynamic. Expression precision is shown in the
middle of Figure 10. The rules can mostly be derived from the type precision. Each
expression is in a precision relation with itself. Structural expressions are in a precision
relation if their sub-expressions are related. Lastly, store precision, shown at the bottomof Figure 10, shows that precision holds if the precision of values in the store holds.

Pragmatic Gradual Polymorphism with Referencesµ; e ,→ s∗ µ′ ; e′

19

(Operational semantics)

Step-evalµ; e ,→ s∗ µ′ ; e′

Step-annov

Step-assignµ; F[e] ,→ s∗ µ′ ; F[e′ ]µ; u : A : A ,→ s∗ µ; u : Aµ; o := v ,→ s∗ µ[o 7→ v]; unit

Step-tap

Step-derefo=v ∈ µµ; ((ΛX. e : A) : ∀X. A) A ,→ s∗ µ; e[X 7→ A] : A[X 7→ A]µ; !o ,→ s∗ µ; v : A

Step-beta

Step-refvo<µµ; ((λx. e : A → B) : A → B) v ,→ s∗ µ; e[x 7→ v] : B : Bµ; ref v ,→ s∗ µ, o = v; o

Step-u|u|µ = A

Step-anno¬value e : Aµ; e ,→ s∗ µ′ ; e′µ; u ,→ s∗ µ; u : Aµ; e : A ,→ s∗ µ′ ; e′ : A

Fig. 11: Reduction rules for λgpr .
Static criteria. We show that the full static type system of λGgpr is equivalent to the
λgpr calculus (Theorem 7). We use s to denote a relation from the static system in caseof ambiguity. Theorem 8 shows the static gradual guarantee of λGgpr . If a more precise
program is well-typed then a less precise program should be well-typed with a lessprecise type.
Theorem 7 (Equivalence for λgpr (statics)). If ·; · ⊨ s e ⇔ A if and only if ·; · ⊢ e ⇔ A.
Theorem 8 (Static Gradual Guarantee). If e1 ⊑ e2 , ·; · ⊢ e1 ⇔ A then ·; · ⊢ e2 ⇔ B
and A ⊑ B.
Dynamic criteria. Theorem 9 says that fully static programs of λGgpr calculus behaves inthe same as the λgpr at run-time. To make the proofs easier, the reduction rules of λgpr
calculus have extra annotations to follow λGgpr (we denoted as s∗). It means that there
are extra identical annotations, as shown in the gray parts of Figure 4. However, theseannotations are identical and they can be removed without affecting the final reduction
result. In addition, as in λGgpr : values have annotations; raw values should step to beannotated values; and annotations are not included in Frames. This requires a few extra
rules, which are shown in Figure 11.
Notably, λGgpr has the dynamic gradual guarantee (Theorem 10). The proof is simple
in comparison to the original proof by Siek et al. [32]. This simple theorem is formalized
following the work of Garcia et al. [12]. It says that if a more precise program with amore precise store can reduce, then the less precise program with a less precise store canalso reduce. Furthermore, their resulting programs and stores should keep the precision
relation.

20

W. Ye, B. C. d. S. Oliveira

Theorem 9 (Equivalence for λgpr (dynamic)). ∀ ·; · ⊨ s e ⇔ A,
– If µ; e ,→ s∗ µ′ ; e′ then µ; e ,→ µ′ ; e′ .
– If µ; e ,→ µ′ ; e′ then µ; e ,→ s∗ µ′ ; e′ .
Theorem 10 (Dynamic Gradual Guarantee). If e1 ⊑ e2 , µ1 ⊑ µ2 , ·; · ⊢ e1 ⇔ A,·; · ⊢ e2 ⇔ B and µ1 ; e1 ,→ µ′1 ; e′1 then there exists e′2 and µ′2 such that µ2 ; e2 ,→ µ′2 ; e′2, e′1 ⊑ e′2 and µ′1 ⊑ µ′2 .

5Discussion

In this section, we briefly discuss alternative designs and possible extensions.
Preserving relational parametricity. An alternative design is to have a directed semantics gradual polymorphism calculi, which preserves parametricity. We employ the eager
semantics similar to the AGT methodology, which is applied in the GSF calculus. Toroet al. [37] analyzed the following example to show how parametricity is broken by thenaive use of the dynamic sealing in the eager semantics:(ΛX.(λx : X.let y : ⋆ = x in let z : ⋆ = y in z + 1)) Int 1
The polymorphic function with type (∀X. X → ⋆) breaks parametricity, which should
be detected at run-time and raise an error. However, the application of the function
reduces to 2. A fresh name variable α is generated and is bounded to the type Int.
Variable x to y is flowing from type Int to type α; y to z is flowing from type ⋆ totype ⋆; and x to z is flowing from Int to ⋆. Any of these type flows are safe. Thus thereason for the loss of parametricity is related to the loss of precise type information.
Consequently, dynamic sealing is not enough to enforce relational parametricity. For
the above example, GSF detects the error by the refining evidences such as (⟨αE1 , αE2 ⟩).
Importantly in the type flow from y to z, more precise types (Int and αInt ) instead of⋆ and ⋆ are obtained, so when moving from x to z the type changes from Int to αInt .
When doing the addition, the run-time error is detected since the flow from αInt to Int
is not defined. A potential approach for us is to use tracked types (A<B1 ,B2 > ), which aresimilar to the refined evidences in the GSF calculus. Because λGgpr is a source language,
we do not have evidences, thus a possible approach is to record information in types.
For the above example, tracked types can track the unknown type with more precise
IntInt
types from y to z to be Int and αInt which is ⋆(Int,α ) and then from x to z to be ⋆(Int,α )as the refined evidences and a run-time error is detected when doing the addition.
A space-efficient gradual polymorphic calculus. Ozaki et al. [27] explored the space
efficiency problem in the gradual polymorphic calculus. They extended the coercion
calculus (λC) [29] with parametric polymorphism (called λC ∀ ). Dynamic sealing wasapplied in λC ∀ to enforce relational parametricity. Consequently, a sequence of coercions is allowed and they showed that it cannot be normalized to a smaller coercion.
In other words, the size of sequences is unbounded. Notably, they stated and provedthat λC ∀ cannot be space-efficient when dynamic sealing is supported. Furthermore,Pragmatic Gradual Polymorphism with References

21

they conjectured that the gradual polymorphic calculus with dynamic sealing cannot
become space-efficient. Our λGgpr calculus substitutes types directly, as the traditionalsemantics without employing dynamic sealing. Moreover, the eager semantics is applied. Thus we believe that it is possible for our λGgpr calculus to be a space-efficient
gradual polymorphic calculus. Two tentative and promising rules are as follows:A∼C¬A ∼ Ce : A : B : C ,→ e : A : C

e : A : B : C ,→ blame

With the above two rules, annotations are removed or an error is raised, to achieve
the space-efficient goal. Surprisingly, with these two rules, it seems possible to have aspace-efficient gradual references calculus naturally. We intend to explore this in the
future.
Implicit polymorphic references. Implicit (higher-rank) polymorphism [10, 19, 26] ispervasive in theoretic and practical programming languages. Existing gradual polymorphic calculi are mainly explicitly polymorphic. One exception is the work of Xie etal. [41]. Explicit polymorphism means that polymorphic types are not related to any of
its instantiated types but in implicit polymorphism, they are related. Xie et al. [41] designed a source gradual implicit polymorphism calculus with consistent subtyping but
their dynamic semantics is defined by translating to the well-known polymorphic blame
calculus (λB∀ ) [3] without the proof of the dynamic gradual guarantee. A possible extension of Xie et al.’s work is to support implicit polymorphism with a direct dynamic
semantics, and to explore the dynamic gradual guarantee and parametricity properties.
However, it is well-known that a naive combination of implicit polymorphism and references lead to an unsound language. A possible solution is to limit polymorphism tosyntactic let-bound values as adopted by Standard ML [40].
Alternative forms of values. In our calculus, all values are annotated, such as 1 : Int or(λx. x : Int → Int) : Int → Int. This introduces some overhead as some annotations are
redundant. We can have an alternative and workable form of values as follows:
v F u | u : ⋆ | (ΛX. e : A) : ∀X. B | (λx. e : A1 → B1 ) : A2 → B2
The above value form removes redundant annotations such as integers (1 : Int). This isgood for performance, but it would make the proof of dynamic gradual guarantee harder.
However, the resulting calculus with fewer annotations should have an equivalent semantics to our calculus, and would be a better candidate for guiding an implementation.

6

Related Work

Gradual typing. Gradual typing is a term coined by Siek et al. [31]. The unknown type?, which we represent as ⋆, is the new notion introduced to a gradual type system tointegrate dynamic and static typing. By using the unknown type ⋆, equality on types
is lifted to consistency. Any type is consistent with type ⋆. Therefore, run-time type

22

W. Ye, B. C. d. S. Oliveira

checking is needed for a gradually typed lambda calculus. Traditionally, the dynamic
semantics of a gradual language is defined by elaborating to a target language, which
includes cast calculi [3, 11, 29, 34, 39] and coercion calculi [13, 14, 27, 29, 30].
Garcia et al. [12] proposed the abstracting gradual typing (AGT) approach, whichallows for deriving a gradual type system by lifting the static type system. They argue
about the weakness of elaborating to a target language, and did not resort to a target language in their calculus by using intrinsic terms. Our λGgpr defines the dynamic
semantics directly without using intrinsic terms, but employing instead an approachbased on type-directed operational semantics (TDOS). Type directed operational semantics (TDOS) was proposed by Huang et al. [15] to design calculi with the merge
operator and intersection types. Ye et al. [42] explored the use of the TDOS in gradualtyping. In TDOS, type annotations are relevant at runtime and can affect the semantics,
unlike many traditional calculi where types are not runtime relevant. With a TDOS wecan design a gradually typed calculus without elaboration to a cast calculus, since thesemantics can be given directly. Our λGgpr employs the eager semantics for higher-ordervalues following an approach similar to AGT. Ye et al. only consider a TDOS for a simply typed, purely functional language. Our work shows that the TDOS approach can beextended to important features, such as polymorphism and references.
Gradual typing with references. Many languages with static and dynamic typing, employing some form of optional typing, support references. These include Flow [8],Dart [6] and TypeScript [5]. However for optional typing, the run-time checking is not
performed for fully dynamic programs, leading to unsoundness with respect to the static
type system. In the work of Siek et al. [31], he already considered mutable references,
but in a very simple setting without annotation expressions. Furthermore, the gradually
typed lambda calculus is elaborated to a target language to define the dynamic semantics. Herman et al. [14] designed a coercion calculus with references, which is space
efficient. A gradualizer, introduced by Cimini and Siek [9], can derive a gradual static
type system and cast insertion with references systematically. Toro et al. [38] designed
source gradual typing system with references λREF
g and a corresponding target language
λϵg using the Abstracting Gradual Typing (AGT) methodology. They designed theREF
λϵg as a space-efficient calculus and proved the gradual guarantee. Our λGgpr is the first
REF
polymorphic gradually typed language with references.
Existing gradual polymorphic calculi. In the following we summarize some of thesolutions to the problem of preserving parametricity and gradual guarantee in gradualpolymorphic calculi and the changes that these solutions entail.
Dynamic sealing. Ahmed et al. [3] solved the problem in Section 2 by using dynamic
sealing, inspired by the work of Matthews et al. [21]. They proposed the polymorphic
blame calculus [3] (we present it as λB∀ ), which is a widely used cast calculus withdynamic sealing. The most interesting construct of λB∀ is the named type binding νX :=A.t, which is introduced to record the instantiated type of a type variable. The programs

Pragmatic Gradual Polymorphism with References

23

in Section 2 behave as expected in λB∀ :(K ⋆ : ⋆ ⇒ ∀X. ∀Y. X → Y → X) Int Int 2 3,→ νY := Int.νX := Int.(2 : X ⇒ ⋆ : ⋆ ⇒ X)∗,→∗ 2
(K ⋆ : ⋆ ⇒ ∀X. ∀Y. X → Y → Y) Int Int 2 3,→∗ νY := Int.νX := Int.(2 : X ⇒ ⋆ : ⋆ ⇒ Y),→∗ blame
The first program succeeds and returns the first argument. While the second program
fails, since the polymorphic information is recorded as X := Int and Y := Int in typebindings and the original type variable names are preserved in the casts. Notably, forhigher-order values, λB∀ follows the lazy semantics as the blame calculus [29,39]. Thatis, for a function value, the checking is delayed until an argument value is applied. This,
unfortunately results in unbounded space consumption for higher-order casts [13, 14].
As Xie et al. [41] pointed out, the compatibility relation of λB∀ mixes explicit andimplicit polymorphism to some extent, since they employ the following rule:A[X 7→ ⋆] ≺ B∀X. A ≺ B
This compatibility rule of λB∀ allows ∀X. X → X to be compatible with any static
instantiated types such as Int → Int and Bool → Bool. These types are not related in
System F so λB∀ is not a conservative extension of System F. The gradual guarantee
has not been discussed in λB∀ , but they show the parametricity property.
The FG and FC calculi. Igarashi et al. [17] improved on λB∀ . They designed a source
calculus (FG ) and a target calculus (FC ), which is a conservative extension of System
F. The dynamic semantics of FG is indirect and defined by translation to FC . FG does
not relate ∀X. X → X with static instantiations, but only with the dynamic instantiation⋆ → ⋆. The type ⋆ → ⋆ is called quasi-polymorphic, since it is an instantiation of∀X. X → X similarly to what happens with implicit polymorphism. However, a typesuch as Int → Int is not quasi-polymorphic. Instead of binding types locally by (νX :=A.t), they made the type bindings global. Their reduction form Σ ▷ f ,→ Σ ′ ▷ f ′ isaugmented with a store, which records the bounded type variables X := A. The above
example reduces in FC as follows.
Σ ▷ (K ⋆ : ⋆ ⇒ ∀X. ∀Y. X → Y → X) Int Int 2 3,→∗ Σ ▷ (ΛX.ΛY.K ⋆ : ⋆ ⇒ X → Y → X) Int Int 2 3,→∗ Σ, X := Int, Y := Int ▷ (K ⋆ : ⋆ ⇒ X → Y → X) Int 2 3,→∗ 2
Furthermore, they argue that type bindings generated locally lead to run-time overheads.
Their observation is that type bindings are not required for every substitution, but only

24

W. Ye, B. C. d. S. Oliveirafor casts with the dynamic type (⋆). Therefore they employ two kinds of type variables, which are distinguished by labels. One kind is static type variables (X::S) and theother kind is gradual type variables (X::G). Type application for static type abstraction
does not generate type bindings, which are only generated for gradual type abstractions.
Parametricity and the static gradual guarantee are proved, although the proofs are notmechanized. However, the dynamic gradual guarantee is left as conjecture. In addition
their static gradual guarantee is proved with some constraints in the type precision relation. In their precision, ∀X. X → X is more precise than ∀X. X → ⋆ but not ∀X. ⋆ → X.
The GSF calculus. Toro et al. [37] presented the gradual polymorphic calculus (named
GSF), which employs the Abstracting Gradual Typing (AGT) methodology. In AGT,
casting of higher-order values is eager compared to λB∀ and FC . This avoids the problem of space consumption although, as New et al. [25] pointed out, the η principle(which ensures V ≡ λx.V x in the call-by-value languages) is broken. To preserve parametricity, global dynamic sealing, which does not distinguish between static and gradual variables, is used. They also refine the presentation of evidence, which witnesses
the consistency judgement, ensuring that it holds. Instead of simple evidences such as(⟨α, Int⟩), they employ sealing evidences (⟨αE , Int⟩). GSF satisfies parametricity but not
the gradual guarantee. Importantly, they proved that the gradual guarantee is incompatible with parametricity.
Parametricity with the Gradual Guarantee. To achieve both parametricity and the gradual guarantee, New et al. [24] designed PolyGv calculus which gave up the syntax of
System F and the users are required to provide different sealing options. They introduced the sealed syntax as sealX M which explicitly seals terms. With the user-definedsyntax, the gradual guarantee and parametricity are proved. More recently, Labrada etal. [20] improve on GSF. They do not change the syntax of System F but insert plausible
sealing forms during the elaboration from a gradual source language which is named
Funk to a target cast calculus. They proved the gradual guarantee and parametricity forthe target language, but for the source language (Funk), the gradual guarantee comeswith a restriction for type applications, which can only be instantiated with base andvariable types. Some of the main theorems are proved in Agda.
Summary. In order to keep parametricity we need several compromises. For instance,
we need to use a dynamic sealing mechanism instead of direct type substitution causing
extra space and time consumption. In many of the earlier calculi, the gradual guarantee is not obtained. In the later calculi, the gradual guarantee is either restricted or weneed to give up the syntax of System F. Traditionally, many works on gradual typing
are based on two different calculi: a source gradually typed language, and a target cast/coercion calculus where casts/coercions are explicit. The dynamic semantics is definedby elaborating the source language to the target calculus. In other words, the semanticsof the gradually typed language is given indirectly via a second, target language. All
previously discussed works follow this indirect way to give the semantics to a gradually
typed source language.
Furthermore, none of the gradually typed polymorphic calculi supports references.
However, even for a static polymorphic calculus extended with mutable references ob-

λB∀

FG

GSF

PolyGv

Funk

λGgpr

2011

2017

2019

2020

2022

present work

Direct Substitution

×

×

×

×

×

✓

System F extension

×

✓

✓

×

✓

✓

Direct Semantics

×

×

×

×

×

✓

Parametricity

✓

✓

✓

✓

✓

×

Gradual Guarantee

×

×

×

✓

✓

-

✓

Semantics

Lazy

Lazy

Eager

Lazy

Eager

Eager

Mechanized Proofs

×

×

×

×

-

Pragmatic Gradual Polymorphism with References✓✓

References

×

×

×

×

×

✓

25

-

Table 1: Comparison among gradual polymorphism calculi. A × denotes no. A ✓ denotes yes while ✓ denotes partial yes.

taining parametricity is highly non-trivial. As Ahmed et al. [2] stated: ”combing mutable references with polymorphism can be extremely tricky.” From the analysis of Jaber
and Tzevelekos [18], we know that naively moving from a polymorphic calculus toincorporate with mutable references, breaks parametricity. The reason is that common
references can be instantiated with differently typed variables. Therefore, extending a
gradual polymorphic calculus with the mutable references is non-trivial, and none of
the existing gradual languages with polymorphism support references.
Table 1 summarizes several features and differences in existing gradually polymorphic calculi.

7

Conclusion

In this paper, we design a static system λgpr with polymorphism and references and its
gradual counterpart λGgpr . λGgpr has a direct semantics without resorting to a cast calculi.
In λGgpr , the gradual guarantee is proved but we give up parametricity. In exchange, ourcalculus can be simplified, since sophisticated mechanisms such as dynamic sealing are
not needed. Our calculus follows the original semantics of System F, based on directtype substitutions, avoiding extra space and time complexity that is necessary by mechanisms such as dynamic sealing. In the future, we could try to find out if there is a way
to keep both gradual guarantee and relational parametricity for the source language, or
explore more efficient formulations of λGgpr .
Acknowledgements We are grateful to anonymous reviewers and our colleagues at theHKU PL group. This work has been sponsored by Hong Kong Research Grants Council
projects number 17209520 and 17209821.

26

W. Ye, B. C. d. S. Oliveira

References
1. Abadi, M., Cardelli, L., Pierce, B.C., Plotkin, G.D.: Dynamic typing in a statically-typed
language. In: POPL ’89 (1989)
2. Ahmed, A., Appel, A.W., Virga, R.: An indexed model of impredicative polymorphism andmutable references (2003)
3. Ahmed, A., Findler, R.B., Siek, J.G., Wadler, P.: Blame for all. In: Proceedings of the 38th
annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp.
201–214 (2011)
4. Barendregt, H.P., Church, A.: The impact of the lambda calculus (2014)
5. Bierman, G., Abadi, M., Torgersen, M.: Understanding typescript. In: European Conference
on Object-Oriented Programming. pp. 257–281. Springer (2014)
6. Bracha, G.: The dart programming language. Addison-Wesley Professional (2015)
7. Cartwright, R., Fagan, M.: Soft typing. In: PLDI ’91 (1991)
8. Chaudhuri, A.: Flow: a static type checker for javascript. SPLASH-I In Systems, Programming, Languages and Applications: Software for Humanity (2015)
9. Cimini, M., Siek, J.G.: The gradualizer: a methodology and algorithm for generating gradualtype systems. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (2016)
10. Dunfield, J., Krishnaswami, N.R.: Complete and easy bidirectional typechecking for higherrank polymorphism. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. p. 429–442. ICFP ’13, Association for Computing Machinery, New York, NY, USA (2013). https://doi.org/10.1145/2500365.2500582, https://doi.org/10.1145/2500365.2500582
11. Garcia, R.: Calculating threesomes, with blame. In: Proceedings of the 18th ACM SIGPLAN
International Conference on Functional programming. pp. 417–428 (2013)
12. Garcia, R., Clark, A.M., Tanter, E.: Abstracting gradual typing. In: Proceedings of the
43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 429–442. POPL ’16, Association for Computing Machinery, New York,NY, USA (2016). https://doi.org/10.1145/2837614.2837670, https://doi.org/10.1145/
2837614.2837670
13. Herman, D., Tomb, A., Flanagan, C.: Space-efficient gradual typing. In: In Trends in Functional Programming (TFP (2007)
14. Herman, D., Tomb, A., Flanagan, C.: Space-efficient gradual typing. Higher-Order and Symbolic Computation 23(2), 167 (2010)
15. Huang, X., Oliveira, B.C.d.S.: A Type-Directed Operational Semantics For a Calculus
with a Merge Operator. In: Hirschfeld, R., Pape, T. (eds.) 34th European Conference on
Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 166, pp. 26:1–26:32. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2020). https://doi.org/10.4230/LIPIcs.ECOOP.2020.26, https://drops.dagstuhl.de/opus/volltexte/2020/13183
16. Huang, X., Zhao, J., Oliveira, B.C.d.S.: Taming the merge operator. Journal of Functional
Programming 31, e28 (2021)
17. Igarashi, Y., Sekiyama, T., Igarashi, A.: On polymorphic gradual typing. Proc. ACM Program. Lang. 1(ICFP) (aug 2017). https://doi.org/10.1145/3110284, https://doi.org/10.
1145/3110284
18. Jaber, G., Tzevelekos, N.: Trace semantics for polymorphic references*. 2016 31st Annual
ACM/IEEE Symposium on Logic in Computer Science (LICS) pp. 1–10 (2016)19. Jones, S.L.P., Vytiniotis, D., Weirich, S., Shields, M.: Practical type inference for arbitraryrank types. Journal of Functional Programming 17, 1 – 82 (2007)

Pragmatic Gradual Polymorphism with References27

20. Labrada, E., Toro, M., Tanter, E., Devriese, D.: Plausible sealing for gradual parametricity. Proc. ACM Program. Lang. 6(OOPSLA1) (apr 2022). https://doi.org/10.1145/3527314,
https://doi.org/10.1145/3527314
21. Matthews, J., Ahmed, A.: Parametric polymorphism through run-time sealing or, theorems
for low, low prices! In: Drossopoulou, S. (ed.) Programming Languages and Systems. pp.
16–31 (2008)
22. Matthews, J., Findler, R.B.: Operational semantics for multi-language programs. ACM
Trans. Program. Lang. Syst. 31(3) (apr 2009). https://doi.org/10.1145/1498926.1498930,
https://doi.org/10.1145/1498926.1498930
23. Møgelberg, R.E., Simpson, A.K.: Relational parametricity for computational effects. Logical
Methods in Computer Science 5, 1–31 (2009)
24. New, M.S., Jamner, D., Ahmed, A.: Graduality and parametricity: together again for the firsttime. Proceedings of the ACM on Programming Languages 4, 1 – 32 (2020)
25. New, M.S., Licata, D.R., Ahmed, A.: Gradual type theory. Proc. ACM Program.
Lang. 3(POPL) (jan 2019). https://doi.org/10.1145/3290328, https://doi.org/10.1145/
3290328
26. Odersky, M., Läufer, K.: Putting type annotations to work. In: POPL ’96 (1996)
27. Ozaki, S., Sekiyama, T., Igarashi, A.: Is space-efficient polymorphic gradual typing possible?
(2021)
28. Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress (1983)
29. Siek, J., Thiemann, P., Wadler, P.: Blame and coercion: Together again for the first time.
In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design
and Implementation. p. 425–435. PLDI ’15, Association for Computing Machinery, New
York, NY, USA (2015). https://doi.org/10.1145/2737924.2737968, https://doi.org/10.
1145/2737924.2737968
30. Siek, J.G., Garcia, R., Taha, W.: Exploring the design space of higher-order casts. In: ESOP(2009)
31. Siek, J.G., Taha, W.: Gradual typing for functional languages. In: Scheme and Functional
Programming Workshop. vol. 6, pp. 81–92 (2006)
32. Siek, J.G., Vitousek, M.M., Cimini, M., Boyland, J.T.: Refined criteria for gradual typing.
In: 1st Summit on Advances in Programming Languages (SNAPL 2015). Schloss DagstuhlLeibniz-Zentrum fuer Informatik (2015)33. Siek, J.G., Vitousek, M.M., Cimini, M., Tobin-Hochstadt, S., Garcia, R.: Monotonic references for efficient gradual typing. In: ESOP (2015)34. Siek, J.G., Wadler, P.: Threesomes, with and without blame. In: Proceedings for the 1st
Workshop on Script to Program Evolution. p. 34–46. STOP ’09, Association for Computing Machinery, New York, NY, USA (2009). https://doi.org/10.1145/1570506.1570511,
https://doi.org/10.1145/1570506.1570511
35. Tobin-Hochstadt, S., Felleisen, M.: Interlanguage migration: from scripts to programs. In:
Companion to the 21st ACM SIGPLAN Symposium on Object-oriented Programming Systems, Languages, and Applications. pp. 964–974 (2006)
36. Tobin-Hochstadt, S., Felleisen, M.: The design and implementation of typed scheme. In:
POPL ’08 (2008)
37. Toro, M., Labrada, E., Tanter, É.: Gradual parametricity, revisited. Proceedings of the ACM
on Programming Languages 3, 1 – 30 (2019)38. Toro, M., Tanter, É.: Abstracting gradual references. Sci. Comput. Program. 197, 102496(2020)
39. Wadler, P., Findler, R.B.: Well-typed programs can’t be blamed. In: European Symposiumon Programming. pp. 1–16. Springer (2009)
40. Wright, A.K.: Simple imperative polymorphism. LISP and Symbolic Computation 8, 343–
355 (1995)

28

W. Ye, B. C. d. S. Oliveira

41. Xie, N., Bi, X., d. S. Oliveira, B.C.: Consistent subtyping for all. ACM Transactions on
Programming Languages and Systems (TOPLAS) 42, 1 – 79 (2018)
42. Ye, W., Oliveira, B.C.d.S., Huang, X.: Type-directed operational semantics for gradualtyping. In: 35th European Conference on Object-Oriented Programming (ECOOP 2021).
Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2021)