Internship proposals

The internships here are all suitable for 5 months full-time research projects. In France, they are most suitable for M2 projects, but can be adapted to M1 projects or L3 projects. Internationally, they are most suitable for Master’s theses, but can be adapted to Bachelor’s theses or summer research internships. 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.

Verified extraction from proof assistants

Different proof assistants such as Rocq, Lean, Agda, and HOL4 can extract code to different programming languages such as OCaml, C, Haskell, and CakeML, amongst others. The extraction process of Rocq to OCaml and the one of HOL4 to CakeML are even verified in the proof assistants themselves. This extraction process is crucial part of the TCB (Trusted Computing Base) of the resulting code, i.e. the programs can only be trusted to fulfill what was proved about them in the proof assistant if the extraction process is correct.

Many of the extraction processes are quite involved, some of them take high effort to produce readable code, others aim at producing code with high performance.

I would be interested in supervising an internship on extraction from Rocq and Lean to CakeML. Since CakeML has a mechanised semantics, it would be possible to verify this extraction process.

Semantics of programming languages

CakeML is defined via functional big-step semantics. I would be interested in supervising an internship on studying how functional big-step semantics can be implemented in Rocq.

Modular meta-theory for the lambda-cube

The mechanisation of the meta-theory of programming lan- guages is still considered hard and requires considerable effort. When formalising properties of the extension of a language, one hence wants to reuse definitions and proofs. But type-theoretic proof assistants use inductive types and predicates to formalise syntax and type systems, and these definitions are closed to extensions. Available approaches for modular syntax are either inapplicable to type theory or add a layer of indirectness by requiring complicated encodings of types.

In past work with Kathrin Stark, we have proposed an approach to modular meta-theory for programming languages based on meta-programming.

This approach allows extending inductive types and predicates after their definition, but it for instance does not allow changing their type.

Since however e.g. the typing predicates of simply typed lambda calculus and System F have different types, changing the type of (inductive) predicates when extending them is crucial.

This internship aims at developing a method for such modular extensions, with the goal to develop a completely modular strong normalisation proof for all languages in Barendregts lambda cube, potentially using normalisation by evaluation.

This internship cannot be continued into a PhD.

Topics in Mechanised Constructive (Reverse) Mathematics

Constructive mathematics works in logical foundations such as the type theory underlying the Rocq proof assistant, where principles like the axiom of choice and the law of excluded middle are not available. As a consequence, every proof of a statement of the form forall x. exists y. f x y = true actually gives rise to an algorithm.

Routinely, principles such as the law of excluded middle are still assumed to prove theorems, but in constructive mathematics one takes care to assume weaker forms of axioms whenever sufficient. Constructive reverse mathematics goes one step further: Whenever one assumes a principle P to prove a theorem T, i.e. P -> T, one immediately also proves that the principle is the weakest possible principle that could have been assumed by showing T -> P.

One interesting topic is Ishihara’s recent characterisation of continuity axioms, stating that every function of type (nat -> nat) -> nat is continuous. Such an axiom is consistent in constructive foundations, and equivalent to the conjunction of various well-known axioms. However, Ishihara’s analysis has not been carried out in type theory, and we conjecture that a type theoretic analysis might require an interesting, fine-grained discussion of countable choice axioms.

These topics could be (co-)supervised by Dominik Kirst in the Inria picube team based at IRIF.

Primitive operations in MetaRocq

Rocq comes with primitive integers, floats, and arrays (Rocq refman 2023). Primitive operations like addition are specified using axioms that however reduce in Rocq’s kernel. MetaRocq (Sozeau et al. 2019), with its formalization of Rocq in Rocq, 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 MetaRocq 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 λ-calculus are either η-convertible, or separable, i.e. there is a λ-term f such that fs evaluates to true and ft 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 Rocq.

potential co-supervision with Beniamino Accattoli

Verified compiler optimisations for functional languages

The CertiRocq project is a verified compiler from Rocq to C. Creating an executable via CertiRocq 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 Rocq programs and in turn implementing and verifying these optimizations as part of the CertiRocq compiler.

potential co-supervision with Zoe Paraskevopoulou

Old internship projects

A specification of Rocq’s guardedness checker: towards a correctness proof (Yee-Jian Tan)

Rocq’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 MetaRocq 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 (Weituo Dai)

In MetaRocq one can write meta-programs (for plugins or tactics) based on raw, untyped syntax of Rocq 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 Rocq 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.

Synthetic Realisability (Sara Rousta)

Realisability is a technique to give interpretations of (constructive) logic via models of computation that allow proving that certain principles such as the law of excluded middle or Markov’s principle are not derivable, or alternatively that they are consistent and can be given a computational interpretation.

Realisability has not been formalised in a proof assistant, most likely due to the overhead it imposes to formalise models of computation such as Turing machines. We conjecture that this burden can be lifted by using a synthetic approach to computability, and want to study different forms of realisability such as Kleene realisability, Kreisel realisability, and Gödel’s dialectica interpretation from this perspective.

This topic could be (co-)supervised by Dominik Kirst in the Inria picube team based at IRIF.

Mechanised Undecidability Proofs for Groups

The word problem for groups is often cited as one of the first purely mathematical problem that were shown undecidable. The proof is independently by Novikov in 1955 and Boone in 1958. Both Novikov and Boone give a proof by reduction directly relying on Turing machines. A simpler proof was given by Britton in 1963, and a proof relying on so called modular machines in 1980 by Aanderaa and Cohen.

The goal of this internship is to identify the simplest undecidability proof for the word problem for groups and mechanise it in the Rocq proof assistant on top of the Rocq library of undecidability proofs.

This topic could be (co-)supervised by Assia Mahboubi (Inria team Gallinette in Nantes).