Strongly Typed System F in GHC

location_city Online schedule Jul 24th 09:00 - 09:45 AM place Grand Ball Room 1

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.

 
 

Target Audience

All

schedule Submitted 1 month ago