| @ | ||
| loic.peyrot | imdea.org |
I work under the supervision of Niki Vazou on (liquid) refinement type systems, more particularly Liquid Haskell. With Colin Rothgang we are defining a translational semantics of Liquid Haskell through a translation to [Rocq].
Previously, I have been a postdoc and PhD student at IRIF, Université Paris Cité.
My last postdoc has been under the supervision of Giuseppe Castagna. I have been working on static type systems for dynamic languages. More concretely, we defined a theory of row polymorphism for type systems with semantic subtyping and set-theoretic types (see the paper).
I did my PhD under the supervision of Delia Kesner. My thesis is centered around two computational models: node replication and generalized applications, both considered as extension of the (untyped) λ-calculus. These extensions have their origin in computational interpretations of proof theory. My coauthors and I develop operational semantics for them, in order to give more concrete implementations of computation, oriented from the perspective of programming languages. Our approach also is guided by non-idempotent intersection type systems. Those can type exactly all terminating programs. We thus obtain a simple model of termination. Considering non-idempotent intersections adds a quantitative analysis of programs, giving for instance bounds on the length of computation and on the size of the results.
You can find my list of publications on DBLP and my thesis here.
