Examples of possible internship subjects

The descriptions below are quite technical; do not hesitate to contact me for more explanations.

Semantics of inductive types

A type theory is typically defined "extrinsically", that is, as a syntax and typing judgements. However, categorical semantics rather rely on a definition of type theories (based on generalised algebraic theories, GATs), which avoids working with untyped syntax completely. Such an "intrinsic" definition can be formalised in type theory using sophisticated inductive types called inductive-inductive types, available in the Agda proof assistant but not in Coq. There are many variations of this intrinsic/extrinsic gap. In some cases, the formal link between the two approaches is formally established (for example, the case of SOGATs in Uemura's phd, or the correspondance between GATs and EATs in Cartmell's phd). We propose to work towards a systematic solution to this problem. Here are some possible research directions.

Mechanisation of category theory

In the theory of programming languages, mechanisation in proof assistants is becoming more and more popular: it brings more confidence about the proofs which are typically large inductions, and makes them directly reusable. Category theory is a major mathematical tool in computer science. Its mechanisation is a challenging task and a typical benchmark for proof assistants. One feature of category theory is that it relies on diagrammatic proofs: they are tedious to translate into formal proofs, as the latter are based on text. We propose to work in line of the CoREACT project to to make diagrammatic reasoning in Coq easier. Here are some possible research directions.

A simple theory of syntax

A free variable can be thought of as a constant mevariable. Therefore, by restricting to closed terms with metavariables, we do not "lose" any information. From a semantic point of view, this suggests a simple notion of specification for syntax as a functor from [Set, Set] to Set, rather than the more involved (standard) notion of pointed strong endofunctor on [Set, Set]. Initial Algebra semantics need to be worked out in this simpler setting. The motivation for this simple theory of syntax comes from a pending attempt to understand the relation between the implementation of a type system involving unification and its mathematical specification.