I am a PhD student in the Gallium team (see our shared research blog!) at INRIA Paris-Rocquencourt, France. My advisor is Didier Rémy.

My main interest is programming languages. I'm familiar with statically typed functional programming languages such as OCaml, or more generally of ML tradition (SML, Haskell...). I'm interested in theoretical aspects of type systems, programming language implementation, general programming language concepts, and even some syntactic aspects. I have a preference for the formalizable aspects, or formalizable approaches to programming language aspects, rather than the often subjective appeal to taste or intuition.

(CV)

- Contact information
- Research themes and documents:
- Types having a unique inhabitant
- Full reduction in the face of absurdity
- Theoretical aspects of mixing GADTs and subtyping in OCaml
- Meta-theory of predicative dependent type theories, using logical relations
- MLF type inference and type-level computation
- A type-safe database library using phantom types

- Teaching

Outside the personal sphere, I communicate by e-mail -- and
interleaved forum, mailing-list or blog posts. Please feel free to
send me an email; I mostly use my Gmail adress, ```
gabriel dot
scherer at gmail
```

.

I'm currently working on the question of knowing whether a given type T has a unique inhabitant -- modulo a given notion of program equivalence. I wrote two blog posts (part 1, and part 2) on the idea. I gave a talk in may 2013 at the PLUME seminar in Lyon, whose slides are available. I discussed some examples applications at the Dependently Typed Programming (DTP'13) Workshop (abstract, slides)

In early 2015 I proposed an algorithm to decide unique inhabitation in the simply-lambda calculus with sums, modulo beta-eta-equivalence. A draft and a prototype implementation are available there.

As a part of this research, I have been looking at the work on multi-focusing for type/proof systems with sum types. You may be interested in a draft (first written in 2013, revised in early 2015) on a correspondence between maximally multi-focused proofs and an equivalence algorithm for simply-typed lambda-calculus by Sam Lindley. I gave an introductory talk on ((maximal) multi-)focusing whose slides are available.

When designing type systems for programming languages, there is often
an unnoticed mismatch between the dynamic semantics we use and the
soundness guarantees given by the type system. We use *weak*
reduction strategies (for implementation reasons or to reason about
side-effect order) but type-soundness would actually hold ("Well-typed
program do not go wrong") if we used *full* reduction, allowing
to reduce under lambdas.

This is all fine, until we end up designing language feature that
break the latter property (safety with respect to *full*
reduction), and we don't notice because we only play with the weak
reduction. It means there is something fundamental about those
features that we haven't noticed/understood, that should be important
for reasoning about programs. GADTs are such a feature.

Didier and I study this question in the following
draft: Full
reduction in the face of absurdity (2014). To technically support
our consideration, this document uses
a *consistent coercion
calculus* as developped by Julien Crétin during
his PhD thesis -- it is a very
convenient and expressive framework in which to study these
issues. For a simplified setting (System F plus logical assumptions),
you may want to look at my
slides (with notes) from the
Journées LTP du GDR
GPL, October 2014.

When GADTs were added by Jacques Garrigue and Jacques Le Normand in OCaml 4.00, we found out that their interaction with subtyping had not been studied theoretically, in particular we were not sure how to soundly assign variances to GADT parameters, and a very restrictive criterion was implement in OCaml. I worked in 2012 on finding the right variance check for GADTs, and this resulted in the article GADTs meet subtyping (arxiv), also available as a long version or slides.

In 2011, I worked with Andreas Abel on meta-theoretical aspects of predicative dependent type theories -- definitional-algorithmic correspondence with logical relations, and universe subtyping and polymorphism. I enjoyed collaborating to his article On Irrelevance and Algorithmic Equality in Predicative Type Theory (arxiv), and also wrote a much less rigorous internship report on the question of universe subtyping.

In a former internship with Didier Rémy at Gallium (2010), I worked
on ML^{F}, an
System F-like type system with type inference; I did
some prototyping and
explored adding F_{ω}-style type-level
operators. A horribly-formated
report is available, but this topic would need some more work
because it raised more questions than it answered.

In June-July 2009, I worked with Jérôme Vouillon on a statically typed domain-specific language for database queries embedded in OCaml, Macaque. The library is publicly available and in a minimal maintainance mode (if bugs are found, they get fixed). We wrote a french-language article for JFLA'10.