Stephanie Weirich, Unversity of Pennsylvania, will give a talk titled: Tracking how dependently typed functions use their arguments.
Overview
- Date:Starts 7 March 2025, 12:00Ends 7 March 2025, 13:00
- Language:English
- Last sign up date:27 February 2025
Abstract
Dependent type systems extend the expressiveness of typed programming languages by allowing the result types of functions to depend on the values of their arguments. This feature allows programmers to design flexible interfaces and express application-specific properties about their code. However, many function arguments in these languages
are purely specificational: they are there to provide information to the type checker, but otherwise have no runtime significance.
These 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.
Registration: by 27 February to be sure to get a lunch sandwich (otherwise no registration needed).
Bio
Stephanie Weirich is a Professor of Computer and Information Science at the University of Pennsylvania. Her research areas include functional programming, type systems, machine-assisted theorem proving, and dependent types. She has served as the General Chair of ICFP 2020, as Program Chair for ESOP 2024, POPL 2019, ICFP 2010, and Haskell 2009, and as an editor for the Journal of Functional Programming, ACM TOPLAS, TheoreTICS, and LMCS. Her honors include the 2022 Milner lecture at the University of Edinburgh, the 2016 ACM SIGPLAN Robin Milner Young Researcher Award, a 2016 Microsoft Outstanding Collaborator award, and the 2016 Most Influential ICFP Paper award.
More information about Stephanie Weirich can be found on University of Pennsylvania's webpage.
