Contract type : Fixed-term contract
Level of qualifications required : PhD or equivalent
Fonction : Post-Doctoral Research Visit
Level of experience : Up to 3 years
About the research centre or Inria department
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.
Context
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)
Assignment
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.
Main activities
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.
Skills
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).
Benefits package
- 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
Remuneration
monthly gross salary amounting to 2746 euros
Share
General Information
- Theme/Domain : Proofs and Verification
- Town/city : Nantes
- Inria Center : Centre Inria de l'Université de Rennes
- Starting date : 2023-10-01
- Duration of contract : 1 year
- Deadline to apply : 2023-06-18
Contacts
- Inria Team : GALLINETTE
-
Recruiter :
Tabareau Nicolas / nicolas.tabareau@inria.fr
About Inria
Inria is the French national research institute dedicated to digital science and technology. It employs 2,600 people. Its 200 agile project teams, generally run jointly with academic partners, include more than 3,500 scientists and engineers working to meet the challenges of digital technology, often at the interface with other disciplines. The Institute also employs numerous talents in over forty different professions. 900 research support staff contribute to the preparation and development of scientific and entrepreneurial projects that have a worldwide impact.
Instruction to apply
Please submit online : your resume, cover letter and letters of recommendation eventually
For more information, please contact nicolas.tabareau@inria.fr
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.