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.