lpeyrot - at - irif.fr
IRIF, office 3010
Bâtiment Sophie Germain
Université Paris Cité, campus Paris Rive Gauche
75013 Paris
About me
Postdoc researcher at the Institut de recherche en informatique fondamentale (IRIF) in Université Paris Cité. I am working on static type systems for dynamic languages. More precisely, I am concerned with the theory and implementation of systems with intersection, union and negation types within the framework of semantic subtyping. I recently obtained my PhD on the operational and quantitative semantics of the λ-calculus, and under the supervision of Delia Kesner.
Current research
With Giuseppe Castagna, we work on adding record polymorphism to type systems with semantic subtyping.
In programming languages with mutable records, the programmer is
allowed to change the structure of records themself, by adding or
removing fields.
From a typing perspective, a classic solution to handle mutation is row
polymorphism.
There, a function can be typed with a polymorphic type
{a:Int|ρ} -> {a:Int|ρ} that will accept as argument any record with a
stricter type, such as
{a:Int, b:Bool} or {a:Int, b:String, c:String},
simply by instantiation of the row variable ρ.
This is effectively a form of subtyping, where types with more
constraints on fields are subtypes of others.
Yet, even in type systems with subtyping (as in our case), a form of
polymorphism on rows is needed for precise typing of mutable records.
Take for instance the following function f that removes the
field a from r (a:_ indicates that the field a
is no longer present in the record).
let f (r:{a:Int}) -> {a:_} = r\af can be applied to any record with at
least a field a storing an integer.
Alas, type information for all fields other than a will be
lost by the application of f, as the result type will
always be {a:_}, for any argument.
With row polymorphism instead, function f will have the
type
{a:Int|ρ} -> {a:_|ρ}.
Thus, information about fields other than a will be stored
in ρ and retrieved in the result type.
Mutable records and subtyping are features already present in the language CDuce. But its type system lacks the precision brought by record polymorphism. The goal of my postdoc is to integrate row polymorphism in the framework of semantic subtyping on which CDuce relies.
In semantic subtyping, we consider an ML-style type system augmented with union, intersection and negation types. Intuition is given by a semantical interpretation. Roughly, types are interpreted as the set of their inhabitants. Subtyping is defined as set inclusion between the interpretations.Challenges arise from the interaction between row polymorphism, set-theoretic types and subtyping.
PhD Thesis
My thesis is centered around two computational models: node replication and generalized applications, both considered as extension of the (untyped) λ-calculus.
These extensions have their origin in computational interpretations of proof theory. My coauthors and I develop operational semantics for them, in order to give more concrete implementations of computation, oriented from the perspective of programming languages.
Our approach also is guided by non-idempotent intersection type systems. Those can type exactly all terminating programs. We thus obtain a simple model of termination. Considering non-idempotent intersections adds a quantitative analysis of programs, giving for instance bounds on the length of computation and on the size of the results.
The λ-calculus is a mathematical model of functional programming languages, with an emphasis on function application. Variants of the calculus are of interest to model specific computational behaviors.
The atomic λ-calculus and the λ-calculus with generalized applications are two (independent) variants of the λ-calculus originating in computational interpretations of proof theory. While programming languages are built from specific deterministic evaluation strategies, the existing literature on the atomic λ-calculus and generalized applications only go over the general theory of the calculi. In particular, reduction of terms is unrestricted, and only analyzed qualitatively. This induces a gap between theory and practice, which we strive to diminish in this thesis.
Starting from the atomic λ-calculus, we isolate the most salient concept of its operational semantics, that we call node replication. This is a particular substitution procedure, which duplicates terms finely, one node of the syntax tree at a time. We follow up with λ-calculi with generalized applications. They use a ternary application constructor, adding a continuation to the usual binary application. In this work, we develop the operational theories built on node replication and generalized applications separately. For the two of them: On an operational level, we give several evaluation strategies, all observationally equivalent to the corresponding strategies in the λ-calculus. On a logical level, our approach is guided by quantitative types. We provide different type systems that inductively characterize semantic properties, but also give quantitative bounds on the length of reduction and the size of normal forms.
More precisely, in the first part of this thesis, we implement node replication by means of an explicit substitution calculus. We show in particular how node replication can be used to implement full laziness, a well-known evaluation strategy for functional programming languages like Haskell. We prove observational equivalence properties relating the fully lazy semantics with the standard ones. In the second part of the thesis, we start with an operational and logical characterization of solvability in λ-calculi with generalized applications. We show how this framework gives rise to a remarkable operational theory of call-by-value. The call-by-name characterization relies on an original calculus with generalized applications. We show in both cases that the operational semantics are compatible with a quantitative model, unlike the one of the original call-by-name calculus. We then prove essential properties of this new call-by-name calculus, and show observational equivalence with the original one.