The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural behavior that boils down to the pervasive functoriality of type formers. We propose and extensively study a type theory, called AdapTT, which makes systematic and precise this idea of functorial type formers, with respect to an abstract notion of adapters relating types. Leveraging descriptions for functorial inductive types in AdapTT, we derive structural laws for type casts on general inductive type formers.
Fri 16 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Fri 16 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:40 | |||
14:00 25mTalk | AdapTT: Functoriality for Dependent Type Casts POPL Arthur Adjedj ENS Paris Saclay, Université Paris-Saclay, Meven Lennon-Bertrand Inria – Université Paris Cité, Thibaut Benjamin Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Kenji Maillard Inria DOI | ||
14:25 25mTalk | Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach POPL DOI | ||
14:50 25mTalk | Encode the Cake and Eat It Too: Controlling Computation in Type Theory, LocallyDistinguished Paper POPL DOI | ||
15:15 25mTalk | Normalisation for First-Class Universe LevelsDistinguished PaperRemote POPL Nils Anders Danielsson University of Gothenburg, Naïm Camille Favier Chalmers University of Technology and University of Gothenburg, Ondřej Kubánek Chalmers University of Technology DOI | ||