GRAPA - Gradual Proof Assistants

The main objective of this French-Chilean research team is to extend the reach of gradual typing to full-fledged type theories in order to support smooth certified programming in a new generation of proof assistants.

The objectives are:

• Internal Reasoning about Precision and Graduality: In this project, we will further develop these initial ideas of internalizing precision and graduality, building upon recent work on observational equality, and extending to other gradual variants of CIC (e.g. with global graduality) in order to demonstrate its benefits. In particular, we will extend our initial results on a cast calculus (GRIP) to a source language akin to GCIC and study the integration of general indexed inductive types in this setting.
• Implementations of Gradual Type Theory: To this date, all advances in gradual dependent types and gradual type theory have been essentially theoretical: there is no implementation of GDTL or GCIC. We aim at addressing this gap, towards usable implementations of gradual type theories for a new generation of proof assistants.

• Nicolas Tabareau, researcher, GRAPA coordinator, project-team GALLINETTE, Inria
• Kenji Maillard, researcher, project-team GALLINETTE, Inria
• Koen Jacobs, Postdoctoral researcher, project-team GALLINETTE, Inria
• Éric Tanter, researcher, GRAPA coordinator, Universidad de Chile
• Stefan Malewski, PhD student, Universidad de Chile
• Tomas Diaz, PhD student, Universidad de Chile