Post-Doctoral Research Visit F - M Category Theory In Type Theory And Vice Versa H/F INRIA

Post-Doctoral Research Visit F/M Category theory in type theory and vice versa
Le descriptif de l'offre ci-dessous est en Anglais
Type de contrat : CDD

Niveau de diplôme exigé : Thèse ou équivalent

Fonction : Post-Doctorant

A propos du centre ou de la direction fonctionnelle

The Inria Rennes - Bretagne Atlantique Centre is one of Inria's eight centres and has more than thirty research teams. The Inria Center is a major and recognized player in the field of digital sciences. It is at the heart of a rich R&D and innovation ecosystem: highly innovative PMEs, large industrial groups, competitiveness clusters, research and higher education players, laboratories of excellence, technological research institute, etc

Contexte et atouts du poste

Within the framework of the ERC project, a package is specifically dedicated to the study of proof transport methodologies and tools in type theory.

The purpose of this project is to investigate how interactive provers based on type theory (Rocq, Agda, Lean, etc.) can be turned into an instrument for producing and checking computer-aided mathematics. The agenda of the present position is to provide a better understanding of how to embody category theory and abstract algebra in type theory, in practice.

Mission confiée

The state of the art in general-purpose, large corpora of formalized mathematics are structured using
hierarchies of algebraic structures. In the style popularized by Bourbaki, mathematical structures attach to
a carrier set some data (e.g., operators of the structure, collections of subsets of the carrier) and prescribed
properties about these data, called the axioms of the structure. The literature describes several attempts to
improve the implementation of inference engines in interactive provers, as well as related programming
methodologies so as to best formalize the notion of mathematical structure. These are necessary
improvements to the design and engineering of interactive provers. Yet they do not suffice to account for
the full power of abstraction provided by category theory and abstract algebra on paper. As a result, formal
proofs still feature lengthy explicit proof scripts that correspond to content left implicit on paper.

This project involves three main axes:

Foundations. Homotopy type theory is a flavor of intentional type theory featuring homotopically moti-
vated axioms and type-theoretic structures. It provides an appealing foundation for mathematics, and has
enabled synthetic approaches to formalized mathematics, previously beyond reach. Several proversare available today for conducting this activity in practice. Some of these provers are implemented as layers
on top of existing ones, like Rocq or Agda, and some are standalone provers. Several important questions re-
garding this type theory and its variants however remain to be investigated further, in particular concerning
reduction and canonicity, whose answers will impact the design of these tools.

Implementation. When a certain logic is understood as an internal language to certain categories with
enough structures, the proofs conducted in the latter logic can be reused in various contexts, with different
meanings. This phenomenon is central to topos theory but no concrete implemented methodology exist
today to reflect this transfer mechanism.

Practice. Existing large corpora of formalized mathematics such as mathlib or Mathematical Compo-
nents are plagued by insufficient support for modularity and abstraction, resulting in a significant amount
of unneeded boilerplate code, as well as avoidable code duplication. We will apply the results obtained in
the previous fundamental axes to concrete use cases from these libraries. In particular, recent advances in
formalized combinatorial algebra has shed light on concrete examples of potential applications.

Principales activités

Main activities (5 maximum) :

- Conduct fundamental research
- Design and develop libraries of formalized mathematics and/or tools for enhancing interactive theorem proving
- Disseminate the advances, in particular by writing scientific papers and delivering talks in relevant venues

Compétences

We are looking for outstanding candidates with a strong expertise in type theory and a good practice
of formalized mathematics using interactive theorem provers based on dependent types. An expertise in
homotopy type theory and cubical type theory would be a clear plus

Avantages

- - Subsidized meals
- Partial reimbursement of public transport costs
- Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
- Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
- Professional equipment available (videoconferencing, loan of computer equipment, etc.)
- Social, cultural and sports events and activities
- Access to vocational training

Rémunération

Monthly gross salary amounting to 2788 euros