GRAPA (short for GRAdual Proof Assistants) is an associate team between the Inria Project-Team Gallinette, led by Nicolas Tabareau, and the Pleiad laboratory of the University of Chile, led by Éric Tanter.

GRAPA is the continuation of a joint line of work between our teams on making proof assistants more accessible by combining static and dynamic checking, combining our expertise on proof assistants on the one hand, and gradual typing on the other hand.

Project

GRAPA aims at extending the reach of gradual typing to full-fledged type theories in order to support smooth certified programming in a new generation of proof assistants.

More specifically, our current objectives are organized around two axes:

  • Foundations of Gradual Type Theory: we develop the foundations of gradual type theory by extending prior work on gradual typing to deal with dependent types as found in the type theories underlying modern proof assistants such as Coq, Agda and Lean. In particular we focus on the Calculus of Inductive Constructions (CIC) and its extensions.
  • Internal Reasoning about Precision and Graduality: we will further develop the 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.
  • Implementations of Gradual Type Theory: we will explore alternatives to implement gradual proof assistants, in particular using extension mechanisms such as rewrite rules and macros.
  • Gradual Verification in Proof Assistants: we will study how to make a program logic such as that of Iris more flexible through hybrid and gradual checking techniques.

News

  • November 25, 2024 to December 5, 2024: Nicolas Tabareau visits Pleiad
  • September 3, 2024: Talk "Gradual Indexed Inductive Types" by Kenji Maillard at ICFP 2024
  • October 16, 2023 to July 31, 2024: Tomás Díaz visits Gallinette
  • April 27, 2024 to July 25, 2024: Mara Malewski visits Gallinette
  • June 19, 2024 to July 3, 2024: Éric Tanter visits Gallinette
  • March 2023: The GRAPA Associate Team is created and funded for the period 2023-2025