- About
- Events
- Calendar
- Graduation Information
- Cornell Learning Machines Seminar
- Student Colloquium
- BOOM
- Fall 2024 Colloquium
- Conway-Walker Lecture Series
- Salton 2024 Lecture Series
- Seminars / Lectures
- Big Red Hacks
- Cornell University - High School Programming Contests 2024
- Game Design Initiative
- CSMore: The Rising Sophomore Summer Program in Computer Science
- Explore CS Research
- ACSU Research Night
- Cornell Junior Theorists' Workshop 2024
- People
- Courses
- Research
- Undergraduate
- M Eng
- MS
- PhD
- Admissions
- Current Students
- Computer Science Graduate Office Hours
- Advising Guide for Research Students
- Business Card Policy
- Cornell Tech
- Curricular Practical Training
- A & B Exam Scheduling Guidelines
- Fellowship Opportunities
- Field of Computer Science Ph.D. Student Handbook
- Graduate TA Handbook
- Field A Exam Summary Form
- Graduate School Forms
- Instructor / TA Application
- Ph.D. Requirements
- Ph.D. Student Financial Support
- Special Committee Selection
- Travel Funding Opportunities
- Travel Reimbursement Guide
- The Outside Minor Requirement
- Diversity and Inclusion
- Graduation Information
- CS Graduate Minor
- Outreach Opportunities
- Parental Accommodation Policy
- Special Masters
- Student Spotlights
- Contact PhD Office
Abstract:
Why should programmers care about dependent types?
Over the past decade, the Haskell compiler GHC has incorporated a number of new type system features inspired by dependent type theory. In this talk, I will motivate this work and demonstrate the benefits of these features through an extended example of a Haskell library for regular expression matching. In the process, I will use this example to analyze what it means for a practical programming language to be "dependently typed."
Bio:
Stephanie Weirich is a Professor of Computer and Information Science at the University of Pennsylvania. She joined Penn after receiving her Ph.D. from Cornell University in 2002. She works in the areas of functional programming, type systems, machine-assisted theorem proving and dependent types. Dr. Weirich has served as the program chair of POPL 2019, ICFP 2010 and the 2009 Haskell Symposium. Her awards include the 2016 Most Influential ICFP Paper award (for 2006) and the 2016 ACM SIGPLAN Robin Milner Young Researcher Award.