Voici une liste non-exostive de sujets potentiels de stages. Si vous êtes intéressés, veuillez contacter
.
- Grader les "arrows" et les profoncteurs :
Keywords: théories des catégories, sémantique dénotationelle, programmation fonctionelle, (co)monades, analyse quantitative, analyse statique
Collaboration: Thomas Seiller, Exequiel Rivas
Level: M2
Prérequis:
Un goût prononcé pour la sémantique dénotationnelle est requis. De bonnes notions en ligique linéaire, systèmes de types, programmations, catégories et/ou analyse statique sont aussi les bienvenues
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 sur la sémentique des systèmes de types linéaires dépedant :
Keywords: programmation fonctionnelle, sémantique dénotationelle, types dépendant, analyse statiquen logique linéaire, analyse quantitative
Collaboration: Damiano Mazza
Level: Mémoire M2
Prérequis:
Un goût prononcé pour la sémantique dénotationnelle est requis. De bonnes notions en ligique linéaire, systèmes de types, programmations, catégories et/ou analyse statique sont aussi les bienvenues
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, en coq, des types ordonnanceurs :
Keywords: types dépendant, formalisation, coq, assistant de preuve, types gradés
Collaboration: Micaela Mayero (LIPN), Dan Ghica (Birmingham)
Level: M1-M2
Prérequis:
Bases de programmation fonctionnelle, logique et assistant de preuves. Expertise dans un sujet plus avancé: coq, types dépendant, annalyse statique.
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.