Tutorials
In the course of my teaching work, I created a few additional materials. In the hope that they might be useful for someone else, I post them here. Please feel free to use or adapt them for your own purposes. LaTeX or Scribble source code available on request.
Converting Regular Expressions to Discrete Finite Automata (2012)
This is a tutorial created for the course Programmer som data (Programs as Data) from ITU in Fall 2012. It is intended to serve as a companion to the course textbook, Peter Sestoft’s Programming Language Concepts.
Tutorial on Polymorphic Type Derivations (2012)
This is a tutorial created for the course Programmer som data (Programs as Data) from ITU in Fall 2012. It is intended to serve as a companion to the course textbook, Peter Sestoft’s Programming Language Concepts. The notation and typing rules are the same as those on page 98 of the book.
Bidirectional Typing Rules (2013)
This tutorial was created to help a student project group understand bidirectional type systems. I couldn’t find any easily accessible literature that made the connection to the type checking algorithm explicit enough and didn’t have too large of a background knowledge requirement. Thus, this tutorial takes a highly operational, low-level approach to build intuitions for programmers.
Checking Dependent Types with Bidirectional Type Checking and NbE (2018)
This tutorial was originally created as notes to accompany a workshop at Code Mesh 2017, and later rewritten in Haskell for the Dependent Types course at PSU in 2019. These notes describe two techniques that are useful for implementing type checkers: normalization by evaluation (NbE) and bidirectional type checking. These notes can additionally be read as an accompaniment to Appendix B of The Little Typer.