This program is tentative and subject to change.
Indexed inductive types are essential in dependently-typed programming languages, enabling precise and expressive specifications of data structures and properties. Recognizing that programming and proving with dependent types could benefit from the smooth integration of static and dynamic checking that gradual typing offers, recent efforts have studied gradual dependent types. Gradualizing indexed inductive types however remains mostly unexplored: the standard encodings of indexed inductive types in intensional type theory, e.g., using type-level fixpoints or subset types, break in the presence of gradual features; and previous work on gradual dependent types focus on very specific instances of indexed inductive types.
This paper contributes a general framework, named PUNK, specifically designed for exploring the design space of gradual indexed inductive types. PUNK is a versatile framework, enabling the exploration of the space between eager and lazy cast reduction semantics that arise from the interaction between casts and the inductive eliminator, allowing them to coexist and interoperate in a single system.
Our work provides significant insights into the intersection of dependent types and gradual typing, by proposing a criteria for well-behaved gradual indexed inductive types, systematically addressing the outlined challenges of integrating these types. The contributions of this paper are a step forward in the quest for making gradual theorem proving and gradual dependently-typed programming a reality.
This program is tentative and subject to change.
Tue 3 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | Type TheoryICFP Papers and Events / JFP First Papers | ||
13:30 18mTalk | Normalization by evaluation for modal dependent type theoryJFP First Paper JFP First Papers Jason Z.S. Hu McGill University, Junyoung Jang McGill University, Brigitte Pientka McGill University DOI | ||
13:48 18mTalk | Closure-Free Functional Programming in a Two-Level Type Theory ICFP Papers and Events András Kovács University of Gothenburg DOI Pre-print | ||
14:06 18mTalk | Gradual Indexed Inductive Types ICFP Papers and Events Mara Malewski Correa University of Chile, Chile, Kenji Maillard Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile | ||
14:24 18mTalk | Dependent Ghosts Have a Reflection for Free ICFP Papers and Events Theo Winterhalter INRIA Saclay | ||
14:42 18mTalk | Static Blame for gradual typingJFP First Paper JFP First Papers Chenghao Su Nanjing University, Lin Chen Nanjing University, Yanhui Li Nanjing University, Yuming Zhou Nanjing University DOI |