Nous cherchons un thésard pour septembre, avec une bourse fournie par le projet. Si vous êtes intéressés, veuillez contacter Flavien Breuvart> Plus d'informations"
Nous avons une bourse pour un postdoc de 1an (malheureusement non extensible). Si vous êtes intéressés, veuillez contacter
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
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.
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
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.
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.