Creating your own language with the lambda calculus as the core.
Implementation
Build and install using stack via stack install
.
Get stack here: http://docs.haskellstack.org/en/stable/README/ (will automatically pull in GHC and all the requirements for you).
Example programs
See programs/simple.lam
and test.lam
.
Rough idea for the list of topics:
-
Session 1: Intro to the syntax and concepts of the lambda calculus, including operational semantics.
-
Session 2: A first implementation: parsing, printing, and interpreting the lambda calculus (written in Haskell) video (Kent only)
-
Session 3: Church encodings (natural numbers, booleans, recursion) and some playing with the implementation. video (Kent only)
-
Session 4: Formally defining a type system via the simply-typed lambda calculus
-
Session 5: Algorithmically defining a type system: type checking and type inference video (Kent only)
-
Session 6: PCF and PCF typing
-
Session 7: The Curry-Howard correspondence in more detail (types vs. logic)
-
Session 8: Call-By-Value vs. Call-By-Name reduction.
-
Session 9: Polymorphism (System F)
-
Session 10: Polymorphic lambda-calculus typing and Theorems for Free.
- Session Y: Implementing ML-style polymorphic types (Hindley-Milner algorithm and related).