Tracking how dependently typed functions use their arguments
By Dr. Stephanie Weirich
Abstract
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.
Bio
Dr. Stephanie Weirich is the ENIAC President’s Distinguished Professor of Computer and Information Science and the University of Pennsylvania. She has made research contributions in the areas of functional programming, type systems, machine-assisted theorem proving, and dependent types. Dr. Weirich has served as the program chair of ESOP 2024, POPL 2018, ICFP 2010, and the 2009 Haskell Symposium and as an editor for the journals TOPLAS, JFP, TheoreTICS, and LMCS. Dr. Weirich is an ACM Fellow and was recognized by the SIGPLAN Milner Young Researcher Award (2016), a Microsoft Outstanding Collaborator award, and a Most Influential ICFP Paper award (awarded in 2016, for 2006).
More information
Recording
Abstract
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.
Bio
Dr. Stephanie Weirich is the ENIAC President’s Distinguished Professor of Computer and Information Science and the University of Pennsylvania. She has made research contributions in the areas of functional programming, type systems, machine-assisted theorem proving, and dependent types. Dr. Weirich has served as the program chair of ESOP 2024, POPL 2018, ICFP 2010, and the 2009 Haskell Symposium and as an editor for the journals TOPLAS, JFP, TheoreTICS, and LMCS. Dr. Weirich is an ACM Fellow and was recognized by the SIGPLAN Milner Young Researcher Award (2016), a Microsoft Outstanding Collaborator award, and a Most Influential ICFP Paper award (awarded in 2016, for 2006).
More information
Recording
Practical information
- General public
- Free
Contact
- Host: Prof. Nate Foster