# PhD Position on Certified Extraction in Nantes

**URL:** https://discourse.rocq-prover.org/t/phd-position-on-certified-extraction-in-nantes/1044
**Category:** Announcements
**Tags:** jobs
**Created:** [September 8, 2020, 2:10pm UTC](https://discourse.rocq-prover.org/t/phd-position-on-certified-extraction-in-nantes/1044 "2020-09-08T14:10:26Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![mattam82](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mattam82/32/11_2.png) [@mattam82](https://discourse.rocq-prover.org/u/mattam82)
#### Post date: [September 8, 2020, 2:10pm UTC](https://discourse.rocq-prover.org/t/phd-position-on-certified-extraction-in-nantes/1044/1 "2020-09-08T14:10:26Z")

</div>

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](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.

Application  
------—————

Applications should be sent on the [jobs.inria.fr](http://jobs.inria.fr) offer at:

[Error](https://jobs.inria.fr/public/classic/en/offres/2020-03002)

Do not hesitate to contact us for more information!

## 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 flaws that prevent extraction from being used  
in complex situations where trust in the extracted code is crucial  
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 bypass 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.