A Type-ical Case Study: The Sound Type-Indexed Type Checker
Please log in to watch this conference skillscast.
The interpreter is a full application, with a parser, type-checker, and evaluator. It serves both as an example of how to use these features and as an existence proof that Haskell is well-suited for fancy-typed programs.
Note: This talk was prepared as a talk, not a workshop. While I very much welcome questions as we go, there is not an explicitly interactive component.
YOU MAY ALSO LIKE:
- Simplifying Constraint Solving in GHC (SkillsCast recorded in November 2020)
- Haskell Fundamentals (2-Day Course) with Alejandro Serrano (Online Course on 5th - 6th July 2021)
- Haskell Fundamentals (4-Day Course) with Alejandro Serrano (Online Course on 8th - 11th November 2021)
- Haskell eXchange 2021 (Online Conference on 16th - 17th November 2021)
- Theorems for Free (SkillsCast recorded in November 2020)
- Comparing Strict and Lazy (SkillsCast recorded in November 2020)
Thank you to our sponsors and partners
Platinum
Gold
Silver
Bronze
A Type-ical Case Study: The Sound Type-Indexed Type Checker
Richard Eisenberg
Richard is a Principal Researcher at Tweag I/O. His research centers around how we can use static type systems to power high-assurance programming and avoid programmer mistakes, all without sacrificing ease-of-use or runtime efficiency. His language of focus is the pure functional language Haskell.
Richard is a core contributor to GHC and serves on the GHC Steering Committee. He lives in suburban Philadelphia with his wife and daughter.