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

• December 6, 2023: Talk "Verified Extraction from Coq to Ocaml" by Nicolas Tabareau at Department of Computer Science, Universidad de Chile

• December 4-15, 2023: Nicolas Tabareau visits Pleiad

• October 27, 2023 to January 25, 2024: Mara Malewski visits Gallinette

• October 16, 2023: Koen Jacobs visits Pleiad

• October 16, 2023 to July 31, 2024: Tomás Díaz visits Gallinette

• March 2023: The GRAPA Associate Team is created and funded for the period 2023-2025