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


Was this useful? Do you want me spending more time working on similar things?

Support me via: