Rencontre, 2 avril 2026
Nous serons en amphi B, sur le site Monod de l'ENS de Lyon.
La rencontre sera diffusée en ligne, des instructions seront disponibles sur cette page peu de temps avant la rencontre.
Programme
-
Mariangiola Dezani (Unviersità di Torino (It))Invited talk: TBA
-
Stephanie Weirich (University of Pennsylvania)
Dependent types increase the expressiveness of programming languages by allowing the result types of functions to depend on the values of their arguments. However, many of these arguments are purely specificational: they are there to provide information to the type checker, but otherwise have no runtime significance. Such arguments can be identified through various mechanisms, such as usage analysis (counting how many times functions use their parameters) or dependency analysis (tracking which results depend on which inputs).
In this talk, I will show how dependent type systems can integrate such analyses and make use of this information. In particular, I will provide an overview of the Dependent Calculus of Indistinguishability (DCOI), a system that uses dependency tracking to identify specificational arguments so that they may be erased at runtime and ignored during conversion.
This is joint work with Yiyun Liu, Jonathan Chan, and Jessica Shi.
