GRAPA - Gradual Proof Assistants

Project Summary

The main objective of this French-Chilean research team is to extend the reach of gradual typing to full-fledged type theories to support smoothly 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) 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.

In France:

• Nicolas Tabareau, researcher, GRAPA coordinator, project-team GALLINETTE, Inria Centre at Rennes University, Inria

• Kenji Maillard, researcher, project-team GALLINETTE, Inria Centre at Rennes University, Inria

• Koen Jacobs, postdoctoral researcher, project-team GALLINETTE, Inria Centre at Rennes University, Inria

In Chile:

• Éric Tanter, researcher, GRAPA coordinator, Universidad de Chile

• Stefan Malewski, PhD student, Universidad de Chile

• Tomas Diaz, PhD student, Universidad de Chile

• https://inria.cl/en/grapa-more-accessible-proof-assistants