Keywords: intersection types, category theory, probabilistic lambda-calculus, linear logic, functional programming
Collaboration: Damiano Mazza, Luc Pellissier
Level: M2
Prerequisites:
A strong taste for category theory and/or denotational semantics is required. Additional notion of Linear Logic, advanced type systems, functional programming and/or measure theory are also welcomed.
The same year, Breuvart and Dal Lago wrote an intersection type system that is sound and complete for the probabilistic λ-calculus. In spite of the strong logical intuitions behind this system, no denotational semantics could be found. In addition, the probabilistic behaviour cannot be encoded correctly in the linear logic, leading to the failure of Mazza et al.’s factorization.
In this internship, we intend to revisit Mazza, Pellissier and Vial’s result and generalize it to extensions of the linear logic in order to factorize Breuvart and Dal Lago’s type system.
This internship can be followed by a PhD fully funded by the ANR CoGITARe on the thematic.
Keywords: category theory, linear logic, denotational semantics, functional programming
Collaboration: Damiano Mazza, Tarmo Uustalu
Level: M2
Prerequisites:
A strong taste for category theory, linear logic and/or denotational semantics is required. Additional notion of advanced type systems and/or functional programming are also welcomed.
This question was partially treated by Breuvart and Pagani [1] in order to create models of graded exponential in a semi-automatic way, but the approach somehow lacked universality a theorem. In a very recent (unpublished) result, Breuvart and Uustalu found a way to fully describe all possible gradations of a given monad under some specific assumptions.
This internship aims at performing the same study for the case of exponentials of linear logic, which is similar but with several additional subtleties coming from the monoidality and the contraction.
This internship can be followed by a PhD fully funded by the ANR CoGITARe on the thematic.
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.
This internship can be followed by a PhD fully funded by the ANR CoGITARe on the thematic.
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.
This internship can be followed by a PhD fully funded by the ANR CoGITARe on the thematic.
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.
This internship can be followed by a PhD fully funded by the ANR CoGITARe on the thematic.
Keywords : combinatorics, tree generation, rewriting, probabilities, random walks, (λ-calculus ?)
Collaboration: Olivier Bodini (team CALIN)
Level: from M1 to M2
Prerequisites: a course on combinatorics (preferably with tree generation of random walks), a course on rewriting or λ-calculus for later phases.
Refs: A first note on the general cases and
a second note on combinatorial details
Given a binary tree, we define a reduction step as choosing a node n(l,r) randomly and uniformally, then duplicating this node into n(n(l,r),n(l,r)). By reproducing this step, we define an alogorism that generates randomly a binary tree. We would like to understand the mean behaviour of this tree. In particular, we conjecture that this tree is growing on average in n.log(n).
In a second time, this result may leads to a fun application in rewiting theory: orthogonal TRSs, when applied a random strategy (redex choosen uniformly at each step), would then respect a 0-1 law, in the sense that any term would have a probability of convergence either 0 or 1.
Going further, we can look at the, more complex, situation of the λ-calculus that is conjectured to verify this 0-1 law.
Keywords : λ-calculus, denotational semantics, computable trees
Collaboration: potentially Giulio Manzonnetto and Thomas Seiller
Level: M2
Prerequisites: a course on denotational semantics (with semantics of the untyped λ-calculus).
Refs: a submited article on relational graph models
A λ-theory is a congruence of λ-terms modulo β-reduction, i.e., it is an equivalent relation ≡ between λ-terms such that ((λx.M)N)≡M[N/x] and such that, whenever M≡M', then λx.M≡λx.M', MN≡M'N and NM≡NM'.
A sufix-prefix-closed sets of computable trees is a set S of (infinite) computable trees of unbounded arrity such that t∈S iff t have a son s∈S.
We conjecture that an important subclass of λ-theories (BT-sensible λ-theories respecting the ω-rule) corresponds exactly to sufix-prefix-closed sets of computable trees, with a conservation of the order.
More specifically, we conjecture that both of these class are equivalent to an intermediate one: the class of relational graph models quotiented by their induced interpretation in the lambda calculus.
mots clefs : réécriture, probabilités, confluence, λ-calcul, catégories, coalgèbre, non-déterminisme, domaines
Collaboration : potentiellement Ichiro Hasuo (Tokyo) et Claudia Fagian (IRIF).
Niveau global : M1 et M2 (en allant plus ou moin loin)
Prérequis : Bases de proba (L2-L3 math) et de réécriture (L3-M1 info). Bonnes capacitées d'abstraction.
Refs: Un petit projet soumis sur la thématique
Généraliser la réécriture vers une version probabiliste peut se faire de différentes manières. La plus commune est de considérer le choix du redex et de la règle appliqué comme probabiliste. Mais ce n’est pas la plus naturelle d’un point de vue langage de programmations et λ-calcul en particulier. Le plus naturel pour cela est de considérer que le redex est choisi non-déterministiquement et que l’on ne fait de tirage probabiliste que pour sa réduction. Par exemple, un opérateur rand ne va se réduire probabilistiquement que lorsque l’on choisi de le réduire.
Dans ce contexte, l'idée serait d’abord d’étudier une notion de réduction multistep remplacement de l’habituelle clôture transitive du small step et obtenue comme une sémantique coalgébrique de trace. Ensuite, nous voulons étudier la notion résultante de confluence, que nous appelons confluence randomisée.
Keywords : linear logic, categorical semantics, dependant types, graded types, denotational semantics
Collaboration: potentially Shin-ya Katsumata (Tokyo)
Level: subect for a these
Prerequisites: an important capacity of abstraction and at least three: a course on linear logic, a course on dependant type systems, a course on category theory, a course on denotational semantics.
Keywords : categorical semantics, dependant types, graded types,
Collaboration: Dan Ghica (Birmingham)
Level: M2
Prerequisites: at least two: a course on linear logic, a course on dependant type systems, a course on category theory, a course on denotational semantics.
Keywords : dependant types, graded types, type theory
Collaboration: Thomas Seiller
Level: M2
Prerequisites: a course on linear logic and a course on dependant type systems.
Keywords : Type systems, OCaml, Categories, (co)Monads,
Collaboration: Jean Vincent Loddo
Level: M2
Prerequisites: a good level on functional programming and manipulation of higher order structures.
Keywords : Type systems, functional programming (OCaml?), Monads,
Collaboration: Jean Vincent Loddo
Level: L3-M1
Prerequisites: a good level on functional programming and manipulation of higher order structures.
The basic idea is to write a modular parser where the modularity is managed by the choice of an embeded monad.
Ultimatelly (especially for a M2 student), we would like to have a revision of major parsing algorithms and to factorise them throw a yet-to-define higher order notion (that can be the notion of monad or a more subtile one).