Here is a non exostive list of potential internship subject. If you are interested, please contact
.
- Toward graded arrows and graded profunctors :
Keywords: category theory, denotational semantics, functional programming, (co)monads, quantitative analysis, static analysis
Collaboration: Thomas Seiller, Exequiel Rivas
Level: M2
Prerequisites:
A strong taste for denotational semantics is required. Additional notion of Linear Logic, advanced type systems, functional programming, category and/or static analysis are also welcomed
The dual notions of parameterised monads and comonads are emerging structures with both a potential for poweful static annalysis, and an extremly clean semantics. However, this apparent "duality" is less obvious when inspected in details. In this intership, we aim at clarifying a bit this duality.
For this, we are interested in arrows, and their categorical interpretations as profunctors. Arrows (and profunctors) can be seen as generalisation of both (non-graded) monads and comonads, giving one of the numerous way to expose their duality. In this internship, we are looking for a graded version which could subsums both graded monads and graded comonads.
- Mémoire on Semantics of Dependent Linear Type Systems :
Keywords: functional programming, denotational semantics, dependents types, static analysis, linear logic, quantitative analysis
Collaboration: Damiano Mazza
Level: Mémoire M2
Prerequisites:
A strong taste for denotational semantics is required. Additional notion of Linear Logic, advanced type systems, functional programming, category and/or static analysis are also welcomed
The so called Dependent Linear type systems are various type systems [GSS92,BucciarelliE01,DLG11,AmorimGHKC17] of similar structures which can be seen as specific but more expressive extensions of what we now call systems with graded comonads [GhicaS11,BrunelGMZ14] and can statically specify strong extensional properties at type level.
Your objective will be to dissect those different systems and extract similitudes and differences, with a particular attention given to the denotational semantics.
The ultimate objective is not required for the internship, but may be part of a PhD thesis (already funded, see below). We are aiming at a unification of those article toward two directions : a parameterised semantics that can be plugged on each of these systems and that contains both flavours of linear logic an dependent type semantics; and a parameterised type system in the style of [GhicaS11,BrunelGMZ14], but with the expressiveness of dependency.
- Formalisation of scheduled types :
Keywords: dependent types, formalisation, coq, proof assistant, graded types
Collaboration: Micaela Mayero (LIPN), Dan Ghica (Birmingham)
Level: M1-M2
Prerequisites:
Bases of functional programming, logic and proof assistants. Expertise in at least one of those more advenced topics: coq, dependant types, static annalysis.
This internship aims at formalising, in Coq proof assistant, an ongoing research project by Breuvart and Ghicca called
Scheduled Types.
A schedule type is a type of the form l1·A1 → l2·A2 → J•B where A1 , A2 and B are scheduled types, where l1 and l2
are labels, and where J is an abstract object called schedule that “represent” the extensional behaviour of the execution of
the programme once given its arguments. A basic example of schedule is a rational expression over the alphabet {l1 , l2 , e}
where e represent an effect, in this case, if J = l2·((e+l2)·l1)* this means that the second argument is always called at the
beginning, then there s an alternation of events with the first being either an effect or a call over the second argument,
and where the second is a call over the first argument. In call-by-name evaluation, these kind of information is crucial for
static analysis. Notice that the schedules can be more complex, but have to respect a certain algebraic structure.
Such type systems are endowed with a complex notion of scope and composition. The associated proofs of subject
reduction and realizability semantics are then extremely intricated. In such situation, making mistakes is quite frequent
and the assistance of a computer is required to verify our proofs: this leads to the need of Coq. Such proofs tend to be
especially smooth in Coq due to their syntactical nature.