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.
Application
------—————
Applications should be sent on the jobs.inria.fr offer at:
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.