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: dependant types, formalisation, coq, proof assistant, graded types Collaboration: Micaela Mayero (LIPN) and Dan Ghica (Birmingham) Level: ~ M1 Prerequisites: Bases of functional programming, logic and proof assistants. Expertise is 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.
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.
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-M2 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).
None yet. Please, feel free to apply !!
He did a small memoir on super monads as well as an educational video on functional programming.