Join Newsletter

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.

Stephanie Weirich

ENIAC President's Distinguished Professor of Computer and Information Science

University of Pennsylvania

United States

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.