We are currectly looking for a PhD student starting in october, the PhD will be funded by the project. If you are interested, please contact Flavien Breuvart. More informations"
We have the funding for a 1y postdoc. If you are interested, please contact Flavien Breuvart.
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
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: 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
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: 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.