View publication

Title Gradualizing the Calculus of Inductive Constructions
Authors Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter
Publication date June 2022
Abstract We investigate gradual variations on the Calculus of
Construction (CIC) for swifter prototyping with imprecise types and terms.
We observe, with a no-go theorem, a crucial trade-off between graduality and
the key properties of normalization and closure of universes under dependent
product that CIC enjoys. Beyond this Fire Triangle of Graduality, we explore
the gradualization of CIC with three different compromises, each relaxing
one edge of the Fire Triangle. We develop a parametrized presentation of
Gradual CIC (GCIC) that encompasses all three variations, and develop their
metatheory. We first present a bidirectional elaboration of GCIC to a
dependently-typed cast calculus, CastCIC, which elucidates the interrelation
between typing, conversion, and the gradual guarantees. We use a syntactic
model of CastCIC to inform the design of a safe, confluent reduction, and
establish, when applicable, normalization. We study the static and dynamic
gradual guarantees as well as the stronger notion of graduality with
embedding-projection pairs formulated by New and Ahmed, using appropriate
semantic model constructions. This work informs and paves the way towards
the development of malleable proof assistants and dependently-typed
programming languages.
Pages 7:1-7:82
Volume 44
Journal name ACM Transactions on Programming Languages and Systems
Publisher ACM Press (New York, NY, USA)
Reference URL View reference page