2020-03002 - Doctorant F/H certified extraction from Coq to OCaml

Type de contrat : CDD

Niveau de diplôme exigé : Bac + 5 ou équivalent

Fonction : 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

The Gallinette team is looking for a highly qualified PhD student to
work on an Inria-Nomadic Labs project on the subject of certified
extraction from Coq to OCaml. The student will be part of the Gallinette
team in Nantes, attached to the Inria Rennes - Bretagne Atlantique
research center (http://gallinette.inria.fr). The thesis will be funded
for 3 years, and the starting date is flexible between October 2020 and
January 2021. The thesis will be co-advised by Nicolas Tabareau,
Pierre-Marie Pédrot and Matthieu Sozeau.

Mission confiée

Thesis subject:

The extraction mechanism from Coq to OCaml can be seen as a compilation
phase, from a functional language with dependent types to a functional
language with a weaker type system. It is very useful to be able to run
and link critical pieces of code that have been certified with the rest
of a software system. Unfortunately, the current extraction mechanism of
Coq suffers from two major flaws that prevent extraction from being used
in complex situations where trust must be preserved and advanced
features of OCaml's type system are used. First, the extraction
mechanism does not make use of new features of OCaml type system, such
as Generalized Abstract Data Types (GADTs). This prevents code using
indexed inductive types (Coq’s generalization of GADTs) to be extracted
to code using GADTs. The second issue comes from the fact that extraction
sometimes produces ill-typed pieces of code (even if it uses Obj.magic
to cheat the type system), for instance when the arity of a function
depends on some value. Therefore, an extracted program can fail to
type-check in OCaml.

The aim of this PhD is to build on the MetaCoq project [SBF+20] to
formally implement an extraction mechanism from Coq to OCaml.  An
important part of the PhD will be to formalize a fragment of OCaml's
type system and operational semantics in Coq and link it with the
existing extraction procedure to untyped terms. To link untyped
extracted code to its corresponding Coq and OCaml types, we will use a
realizability approach and the notion of semantic typing (as pioneered
in the RustBelt project). Based on this, we expect to show how to
extract (a subset of) Coq's inductive familes to OCaml GADTs while
dealing with the difference between these two language features.

[SBF+20] Coq Coq Correct: Verification of Type Checking and Erasure for
Coq, in Coq. M. Sozeau, S. Boulier, Y. Foster, N . Tabareau,
T. Winterhalter. POPL'20, New-Orleans, USA.

Principales activités

Principales activés (5 maximum) :

Activités complémentaires (3 maximum) :

 

Exemples d'activités :

  • Analyser les besoins des {partenaires, clients, usagers}
  • Proposer des solutions **** pour ****
  • Développer des programmes/ des applications/ des interfaces de ****, ****
  • Concevoir des plateformes expérimentales ****
  • Rédiger la documentation
  • Rédiger les rapports
  • Rédiger ****
  • Tester, modifier jusqu’à valider
  • Diffuser le(s) **** vers **** via ****
  • Former à l’utilisation les principaux clients du service
  • Animer une communauté d’utilisateurs
  • Présenter l’avancée des travaux aux partenaires, **** devant un public de financiers ****
  • Autre ****

Compétences

Compétences techniques et niveau requis :

Langues :

Compétences relationnelles :

Compétences additionnelles appréciées :

Avantages

  • Subsidised catering service
  • Partially-reimbursed public transport

 

Rémunération

monthly gross salary amounting to 1982 euros for the first and second years and 2085 euros for the third year