Strongly Typed System F in GHC
YOW! Lambda Jam 2020
There are many examples that demonstrate how to create a strongly typed abstract syntax in Haskell for a language with a simple type system. But there are many fewer examples that allow the embedded language to be polymorphic. I will work through what it takes to do so, touching on variable binding representations, and exploring the limits of dependently-typed programming in GHC.
ENIAC President's Distinguished Professor of Computer and Information Science
University of Pennsylvania
Stephanie is the ENIAC President's Distinguished Professor of Computer and Information Science at the University of Pennsylvania. Her research interests include statically-typed functional programming, dependent types, interactive theorem proving and programming language theory. She is the General Chair of ICFP 2020 and hopes to see you (virtually) in August.