(Last page update: May 2024.)
Amélie Rima, 2023-current, co-supervised
with Paolo
Pistone at ENS Lyon.
Amélie works on canonical
representations for System F.
Clément Allain, 2024-current.
Clément works on reasoning about
the correctness of tricky programs, including the TRMC
transformation, unsafe language features, and concurrent data
structures.
(Joint article: Dynarray)
Olivier Martinot,
2020-current.
Olivier works on constraint-based type inference
for GADTs.
(Joint workshop abstracts: quantified applicatives,
frozen constraints)
Abdelkader Belloundja, summer 2024, M2 internship.
Abdelkader
works on a binary version of Higher-Order Model Checking to try to
decide relational properties, in particular program equivalence.
Tom Soucies, summer 2022, L3 internship.
Tom worked turning
the OCaml parsetree interpreter
of Camlboot into
an interpreter of the typedtree.
(code)
Nicolas Chataing, summer 2021, M2 internship.
Nicolas worked
on designing and implementing an OCaml feature suggested by Jeremy
Yallop, namly single-constructor unboxing -- unboxing some
constructors in a variant type, after checking that they do not
introduce conflicts of value representation.
(Jeremy's RFC,
our prototype implementation,
publication)
Maxime
Legoupil, summer 2021, M2 internship.
Maxime worked on
checking that the simply-typed $\lambda$-calculus with sums indeed
forms a cartesian category of contexts and simultaneous
substitutions. This requires subtle/tricky work to define hereditary
substitutions in presence of sums, whose termination is unclear.
Simon Colin, spring 2020, M1 internship.
Simon working on
extending the [@@unboxed] annotation on
single-constructor variants or single-field records in OCaml. The
type-checker needs to check that the unboxing will not result in
a naked float value, and the check would previously not
support mutually-recursive type definitions. Simon worked on
rigourously describing the analysis as a system of inference rules,
and its extension to mutually-recursive definition. I worked with
Rodolphe Lepigre on implementing it in the OCaml compiler.
(PR,
publication.)
Ulugbek Abdullaev,
summer 2020, Outreachy internship, remote.
Ulugbek worked on
extending
the efftester
prototype of Jan Midtgaard. efftester generates random
programs in a fragment of OCaml that are known to have a unique
evaluation order, to perform differential testing of OCaml
implementations.
(code)
Francesco Mecca,
spring-summer 2020, M1 internship.
Francesco worked on
a translation-validation approach to checking the correctness of
a fragment of the OCaml pattern-matching compiler.
(code,
workshop abstract)
Alban Reynaud, summer 2018, L3 internship.
Alban worked on
a simpler presentation of a static analysis proposed by Jeremy
Yallop to accept or reject OCaml recursive value declarations.
(PR,
publication.)
Bryce Clarke,
2022-2024, co-supervised with Noam
Zeilberger. We worked on a proof-theoretic construction of the
free bifibration over a given functor.
(workshop abstract)
Luc Pellissier, 2019-2020.