- Factorizing probabilistic intersection types :
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.
Mazza, Pellissier and Vial showed, two years ago, that most intersection types systems in the literature could be factorized into the choice of an encoding of the calculus into linear logic proof net and the choice of a polyadic interpretation of those proof-net (a decomposition similar to Taylor expansion). This factorization arises in the highly abstract categorical framework of Cat-operads (Cat-enriched colored operads) in which they apply Grothendieck construction to transport the two into composable morphisms. The strength of this construction is that it assures the soundness and completeness of the intersection type system for the considered calculus.
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.
- Gradder les exponentiels de la logique linéraire :
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.
The dual notions of graded monads [3] and linear logic exponentials [4, 2] are emerging structures with both a potential for powerful static analysis, and an extremely clean semantics. The examples in the literature, however, are often quite simple and very similar. In order to analyze the expressive power of those gradation, a natural question is to ask what are the gradation refining a given monad/exponential.
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.
- 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.
This internship can be followed by a PhD fully funded by the ANR CoGITARe on the thematic.
- 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.
This internship can be followed by a PhD fully funded by the ANR CoGITARe on the thematic.
- 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.
This internship can be followed by a PhD fully funded by the ANR CoGITARe on the thematic.
- Randomised strategies and 0-1 law :
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.
- λ-theory and sufix-prefix-closed sets of computable trees :
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.
- Confluence Randomisée Pour des Réductions aléatoires :
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.
- Localy linear categories :
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.
- Categorical semantics of scheduled types :
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.
- Adding dependancy to scheduled types :
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.
- Categorical formalisation of a concurent system with joint memory :
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.
- A monadic parser :
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).