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.

Design categorical semantics for untyped syntax and typing judgements;
Define a direct semantic translation from inductive-inductive types to indexed inductive types and/or other variants;
Explore variants of the construction (in Agda) of finitary inductive-inductive types from indexed inductive types.
Handle sort equations in the constructions of GATs from EATs. This can be used to formalise a type theory with Russel universes, as in Coq or Agda.
Design a type theory where inductive types are first-order objects, so that it makes it possible to formalise the theory of inductive types.

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.

Improve a prototypical diagram editor, which already supports basic generation of Coq proof scripts from diagrams drawn by the user (see here for more explanations);
Develop a Coq library to make mechanisation of string diagrams easier;
Mechanise category theory in Coq using this editor and hierarchy builder, a state-of-the-art Coq tool to help building hierarchies of algebraic structures. A possible benchmark would be MacLane's coherence theorem for monoidal categories. Another interesting challenge is the mechanisation of locally presentable categories, a ubiquitous categorical notion, based on recent work on constructive ordinals.
Exploit this library to mechanise some results in the theory of programming languages. This could involve, for example, mechanising recent categorical semantics of "pattern unification", a decidable fragment of higher-order unification used in major proof assistants:
- Formalise a correctness proof of the algorithm.
- In particular, implement a structurally recursive pattern unification algorithm in the style of McBride first-order unification algorithm to justify termination.
- Design categorical semantics for Qian's efficient pattern unification algorithm, where terms are DAGs rather than trees, in the spirit of "Initial Algebra Semantics for Cyclic Sharing Tree Structures".
- Extend the semantics to cover dependently typed languages

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.