Fri 21 Jan 2022 14:20 - 14:45 at Salon I - TOPLAS Session Chair(s): Andrew C. Myers

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 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.

Fri 21 Jan

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 14:45
TOPLAS SessionPOPL at Salon I
Chair(s): Andrew C. Myers Cornell University
13:30
25m
Talk
Armed cats: formal concurrency modelling at ArmRemote
POPL
Jade Alglave University College London, Will Deacon ARM Ltd., Richard Grisenthwaite , Antoine Hacquard EPITA, LRDE, Luc Maranget Inria
13:55
25m
Talk
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs Remote
POPL
Emanuele D'Osualdo MPI-SWS, Julian Sutherland Imperial College London, Azadeh Farzan University of Toronto, Philippa Gardner Imperial College London
DOI
14:20
25m
Talk
Gradualizing the Calculus of Inductive ConstructionsRemote
POPL
Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Kenji Maillard Inria Nantes & University of Chile, Nicolas Tabareau Inria, Éric Tanter University of Chile