ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Mon 12 Sep 2022 16:10 - 16:30 at Linhart - (Gradual) Type Theory Chair(s): Jesper Cockx

Gradualizing the Calculus of Inductive Constructions (CIC) involves dealing with subtle tensions between normalization, graduality, and conservativity with respect to CIC. Recently, GCIC has been proposed as a parametrized gradual type theory that admits three variants, each sacrificing one of these properties. For devising a gradual proof assistant based on CIC, normalization and conservativity with respect to CIC are key, but the tension with graduality needs to be addressed. Additionally, several challenges remain: (1) The presence of two wildcard terms at any type-the error and unknown terms-enables trivial proofs of any theorem, jeopardizing the use of a gradual type theory in a proof assistant; (2) Supporting general indexed inductive families, most prominently equality, is an open problem; (3) Theoretical accounts of gradual typing and graduality so far do not support handling type mismatches detected during reduction; (4) Precision and graduality are external notions not amenable to reasoning within a gradual type theory. All these issues manifest primally in CastCIC, the cast calculus used to define GCIC. In this work, we present an alternative to CastCIC called GRIP. GRIP is a reasonably gradual type theory that addresses the issues above, featuring internal precision and general exception handling. GRIP features an impure (gradual) sort of types inhabited by errors and unknown terms, and a pure (non-gradual) sort of strict propositions for consistent reasoning about gradual terms. By adopting a novel interpretation of the unknown term that carefully accounts for universe levels, GRIP satisfies graduality for a large and well-defined class of terms, in addition to being normalizing and a conservative extension of CIC. Internal precision supports reasoning about graduality within GRIP itself, for instance to characterize gradual exception-handling terms, and supports gradual subset types. We develop the metatheory of GRIP using a model formalized in Coq, and provide a prototype implementation of GRIP in Agda.

Mon 12 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

15:50 - 16:50
(Gradual) Type TheoryICFP Papers and Events at Linhart
Chair(s): Jesper Cockx TU Delft
15:50
20m
Talk
Propositional Equality for Gradual Dependently Typed Programming
ICFP Papers and Events
Joseph Eremondi University of British Columbia, Ronald Garcia University of British Columbia, Éric Tanter University of Chile
DOI
16:10
20m
Talk
A Reasonably Gradual Type Theory
ICFP Papers and Events
Kenji Maillard Inria Nantes & University of Chile, Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Nicolas Tabareau Inria, Éric Tanter University of Chile
DOI
16:30
20m
Talk
A completely unique account of enumeration
ICFP Papers and Events
Cas van der Rest Delft University of Technology, Wouter Swierstra Utrecht University, Netherlands
DOI