Defence & Jury Information

The defence will take place on November 9th, 2021, at 5p.m. Paris Time (UTC+1), both physically and online.
Physically: in Room 3052, Bâtiment Sophie-Germain, Université de Paris.
Online: on Zoom, using this link.

The members of the jury are:

Abstract

In this thesis, we study the interaction between set-theoretic types and gradual typing. Set-theoretic types are types containing union, intersection, and negation connectives, which are useful to type several programming language constructs very precisely. For example, union types can be used to give a very precise type to a conditional instruction, while intersection types can encode function overloading. On the other hand, gradual typing allows a programmer to bypass the type-checker, which can be useful when prototyping.

Set-theoretic types are well-suited to a semantic-based approach called "semantic subtyping", in which types are interpreted as sets of values, and subtyping is defined as set-containment between these sets. We adopt this approach throughout the entirety of this thesis. Since set-theoretic types are characterized by their semantic properties, they can be easily embedded in existing type systems. This contrasts with gradual typing, which is an intrinsically syntactic concept since it relies on the addition of a type annotation to inform the type-checker not to perform some checks. In most of the existing literature, gradual typing is added by extending the subtyping relation in a syntactic way. This makes the approach very difficult to extend and generalize as this heavily depends on the system at hand.

In this thesis, we try and reconcile the two concepts, by proposing several semantic interpretations of gradual typing. The manuscript is divided into two parts. In the first part, we propose a new approach to integrate gradual typing in an existing static type system. The originality of this approach comes from the fact that gradual typing is added in a declarative way to the system by adding a single logical rule. As such, we do not need to revisit and modify all the existing rules. We then propose, for each declarative type system, a corresponding algorithmic type system, based on constraint solving algorithms. We illustrate this approach on two different systems. The first system is a Hindley-Milner type system without subtyping. We present a gradually-typed source language, a target language featuring dynamic type checks (or "casts"), as well as a compilation algorithm from the former to the latter. We then extend this language with set-theoretic types and subtyping on gradual set-theoretic types, and repeat this presentation.

In the second part of this manuscript, we explore a different approach to reconcile set-theoretic types and gradual typing. While the first part of the thesis can be seen as a logical approach to tackle this problem, the second part sets off along a more semantic strategy. In particular, we study whether it is possible to reconcile the interpretation of types proposed by the semantic subtyping approach and the interpretation of the terms of a language. The ultimate goal being to define a denotational semantics for a gradually-typed language. We tackle this problem in several steps. First, we define a denotational semantics for a simple lambda-calculus with set-theoretic types, based directly on the semantic subtyping approach. This highlights several problems, which we explain and fix by adapting the approach we used. We then extend this by giving a formal denotational semantics for the functional core of CDuce, a language featuring set-theoretic types and several complex constructs, such as type-cases, overloaded functions, and non-determinism. Finally, we study a gradually-typed lambda-calculus, for which we present a denotational semantics. We also give a set-theoretic interpretation of gradual types, which allow us to derive some very powerful results about the representation of gradual types.