Functional Programming and Proof Checking Course Plan

How to read this

Entry format:

* <text> | <resources to read>

Introduction

There are two ways to learn:

We’ll try to switch between these two approaches in class. Here is the plan.

Introduction to Haskell

Introduction to untyped λ-calculus

Resources: first 50 pages or so from TTFP, first sections from Selinger’s notes, first chapters from Sørensen, Uzryczyn.

Simply-typed λ-calculus (λ → )

Resousces: barendregt, thompson-ttfp, sorensen-urzyczyn, semssm, damas-milner, ptihr, tiic, tiioc.

Primitive Haskell

Resources: typeclassopedia, gentle-introduction-to-haskell, gentle-introduction-to-haskell-ru-1, gentle-introduction-to-haskell-ru-2.

Hindley-Milner and Type Classes

Monads and Arrows

Resources: corresponding chapters from Gentle, monads-as-computation, monads-as-containers, typeclassopedia, arrows, fop.

Haskell Programs on a Real Hardware. GHC Hacking

Resources: ghc-user-guide, especially ghc-using-ghc chapter.

Making Haskell Programs Fast

Introduction to Agda

Primitive Agda

Needs more logic