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.

Every year Inria International Relations Department has a few postdoctoral positions in order to support Inria international collaborations.

This year, postdoctoral positions within the frame of Inria London, Inria Brasil and Inria Chile programs and to strengthen partnerships with Simula (Norway), University of Waterloo (Canada) and KAIST and ETRI (South Korea) are eligible.

The postdoc contract will have a duration of 12 to 24 months. The default start date is November 1st, 2023 and not later than January, 1st 2024. The postdoctoral fellow will be recruited by one of the Inria Centers in France but it is recommended that the time is shared between France and the partner’s country (please note that the postdoctoral fellow has to start his/her contract being in France and that the visits have to respect Inria rules for missions)

Candidates for postdoctoral positions are recruited after the end of their Ph.D. or after a first post-doctoral period: for the candidates who obtained their PhD in the Northern hemisphere, the date of the Ph.D. defense shall be later than 1 September 2021; in the Southern hemisphere, later than 1 April 2021.

In order to encourage mobility, the postdoctoral position must take place in a scientific environment that is truly different from the one of the Ph.D. (and, if applicable, from the position held since the Ph.D.); particular attention is thus paid to French or international candidates who obtained their doctorate abroad.

Exploring variants of the internal theory of proof assistants such as Aida, Coq or Lean is an active area of research. From cubical type theory to give a computational content to the univalent foundations, to the addition of exceptions and dynamic type casting for gradual certification.

Implementing a new proof assistant from scratch is a huge undertaking, both costly and complex, which can prevent quick experimentation with the new theory. It is therefore preferable to be able to rely on an existing proof assistant. To implement a novel type theory in a proof assistant there are two main alternatives: (1) to modify the internals of the proof assistant or (2) to use its extension mechanisms. The most appealing is of course to use its extension mechanisms, provided that they are sufficiently expressive and powerful to define the theory.

Mechanisms such as notations in Coq, Agda or Lean provide only some limited syntactic extensions, which are insufficient for many purposes. A more powerful approach for syntactic extensibility are macros [Clinger and Rees 1991; Flatt 2002, 2016; Hart 1963; Hieb et al. 1992; Kohlbecker et al. 1986]. Some metaprogramming tools such as MetaCoq [Sozeau et al. 2020] only work for well-typed terms already existing in the native type theory and therefore cannot be used to introduce whole new constructs. Nevertheless, recent developments in extension mechanisms for proof assistants, such as rewrite rules[Cockx et al. 2021] and macros [Chang et al. 2019; Ullrich and De Moura 2022], do appear to be a promising approach in integrating novel elements to these systems. Coq currently supports neither rewrite rules nor macros. Rewrite rules are currently available only in an experimental branch, while macros have not been considered at all. An objective of this project is to contribute to the development of a novel macro system for Coq and integrate both macros and rewrite rules within MetaCoq.

Furthermore, some extensions require adding effects, such as exceptions, or new reasoning principles (such as univalence) to the underlying type theory. This is not a simple task because proof assistants lack logical modularity. The problem is that there is no way to introduce possibly incompatible reasoning principles and have them safely cohabit without endangering their metatheoretical properties. Recent unpublished work has proposed the multiverse framework [Maillard et al. 2021] where each principle can be encapsulated into different universe hierarchies in a way that they can interact safely. A goal of this project is to further develop the initial idea of the multiverse and realize it in Coq, in a way that complements and integrates with the extension mechanisms described above.

The candidate is expected to have good knowledge of an interactive proof assistant (preferably Coq, but Lean or Agda are also fine), and good notion of functional programming (preferable OCaml).

• Subsidized meals
• Partial reimbursement of public transport costs
• Possibility of teleworking (90 days per year) and flexible organization of working hours
• Partial payment of insurance costs

monthly gross salary amounting to 2746 euros