Master internship proposals

The internships here are all suitable for M2 projects. Most can be adapted to M1 projects, L3 projects, or master project in other countries. I am happy to discuss all of these options, just contact me by email.

Also feel free to contact me to suggest your own ideas about projects.

I might have PhD funding available for September 2024, feel free to contact me.

A specification of Coq’s guardedness checker: towards a correctness proof

Coq’s guardedness checker is crucial for its consistency. However, there is no accessible mathematical specification for it, and consequently no proofs about it exist.

This project is about specifiying the guard checker using MetaCoq abstractly, implementing it as a program, and showing that the program implements the abstract specification.

If time allows, we could then work on future steps on showing that a program satisfying the guard condition can be translated to a theory with a weaker form of recursion (Gimenez 2007).

Meta-programming with scope and type guarantees

In MetaCoq one can write meta-programs (for plugins or tactics) based on raw, untyped syntax of Coq terms. One can then prove that the resulting programs are well-typed or do not contain free variables, or have other semantic properties.

Instead of proving these properties after the fact, it would be interesting to immediately provide such guarantees at the time of implementing the meta-programs, e.g. via a type of well-typed terms or well-scoped Coq syntax.

This internship aims at using several approaches to define such types with guarantees for the user, compare and contrast them, and implement case studies using them.

Primitive operations in MetaCoq

Coq comes with primitive integers, floats, and arrays (Coq refman 2023). Primitive operations like addition are specified using axioms that however reduce in Coq’s kernel. MetaCoq (Sozeau et al. 2019), with its formalization of Coq in Coq, verified type checker, and verified extraction procedure, does not cover primitive operations, i.e. they are treated as irreducible axioms. We would like to extend the theory of MetaCoq with reducible primitive operations, with the final goal of extending the correctness proof of extraction to OCaml.

Formal proof of Böhm’s theorem

Böhm’s theorem, due to Corrado Böhm (1968), states that any two normal forms $s,t$ in $\lambda$-calculus are either $\eta$-convertible, or separable, i.e. there is a $\lambda$-term $f$ such that $f s$ evaluates to true and $f t$ evaluates to false.

Gerard Huét (1993) has given a constructive proof of the theorem, witnessed by a CAML program proved correct on paper.

This internship aims at re-developping and potentially improving Húet’s argument by immediately giving the proof and verifying the algorithm in Coq.

Verified compiler optimisations for functional languages

The CertiCoq project is a verified compiler from Coq to C. Creating an executable via CertiCoq tends to result in slower programs than using extraction to OCaml and the OCaml compiler. Likely, this is due to optimisations the OCaml compiler runs.

This internship aims at analyzing which optimisations have the biggest impact for extracted Coq programs and in turn implementing and verifying these optimizations as part of the CertiCoq compiler.