Gradualizing the Calculus of Inductive Constructions

Abstract: (joint work with M. Bertrand, K. Maillard, N. Tabareau)

Acknowledging the ordeal of a fully formal development in a proof assistant such as Coq, we investigate gradual variations on the Calculus of Inductive Construction (CIC) for swifter prototyping with imprecise types and terms. We observe, with a no-go theorem, a crucial tradeoff between graduality and the key properties of canonicity, decidability 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 that encompasses all three variations, and jointly develop their metatheory. We first present a bidirectional elaboration of Gradual CIC to a dependently-typed cast calculus, which elucidates the interrelation between typing, conversion, and graduality. We then establish the metatheory of this cast calculus through both a syntactic model into CIC, which provides weak canonicity, confluence, and when applicable, normalization, and a monotone model that purports the study of the graduality of two of the three variants. This work informs and paves the way towards the development of malleable proof assistants and dependently-typed programming languages.

[The talk will be on the “intro material” of the paper, namely the analysis that leads to the Fire Triangle, and not on the gory technical details of the metatheory of Gradual CIC]

Spanishlogic in computer scienceprogramming languages

Audience: researchers in the topic

LoReL Seminar

Series comments: Talks are either in Spanish or English, however they can often be in English upon request.