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 inductiveinductive 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 inductiveinductive types to indexed inductive types and/or other variants;

Explore variants of the construction (in Agda) of finitary inductiveinductive 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 firstorder 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 stateoftheart 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 higherorder unification used in major proof assistants:
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.