Functional Programming and Proof Checking Course Plan

by Jan Malakhovski

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 λ\lambda-calculus

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

Simply-typed λ\lambda-calculus (λ\lambda_{\to})

Resousces: ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps, https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385, http://www.win.tue.nl/~hzantema/semssm.pdf, http://www.cs.cmu.edu/~crary/819-f09/DamasMilner82.pdf, http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/index.htm, https://personal.cis.strath.ac.uk/adam.gundry/type-inference/, http://requestforlogic.blogspot.com/2010/10/type-inference-in-and-out-of-context.html.

Primitive Haskell

Resources: http://www.haskell.org/haskellwiki/Typeclassopedia, http://www.haskell.org/tutorial/, http://www.rsdn.ru/article/haskell/haskell_part1.xml, http://www.rsdn.ru/article/haskell/haskell_part2.xml.

Hindley-Milner and Type Classes

Monads and Arrows

Resources: corresponding chapters from Gentle, http://www.haskell.org/haskellwiki/Monads_as_computation, http://www.haskell.org/haskellwiki/Monads_as_containers, http://www.haskell.org/haskellwiki/Typeclassopedia, http://www.cse.chalmers.se/~rjmh/Papers/arrows.pdf, http://www.soi.city.ac.uk/~ross/papers/fop.html.

Haskell Programs on a Real Hardware. GHC Hacking

Resources: http://www.haskell.org/ghc/docs/latest/html/users_guide/index.html, especially http://www.haskell.org/ghc/docs/latest/html/users_guide/using-ghc.html chapter.

Making Haskell Programs Efficient

Introduction to Agda

Primitive Agda

Needs more logic