The course consists of two major parts:

Theory: fundamental theories of PL: lambdacalculus and PCF,
formal semantics, program analysis, type systems and theory.

Functional programming: Haskell will be our language.
This part includes important concepts of functional programming, FP data structures and algorithms,
functional pearls, etc.
After the course, students will be expected to have a good understanding of the elementary
theory of programming languages and be able to use related techniques to do basic program analysis.
On the practical side, they should have a deep understanding of concepts of functional programming,
and be able to use a functional language to develop applications of reasonable size.
Reference
We do not have a textbook for the course. Here are some references.
Lecture notes and related material will be available on this page while the course goes on.
Theory
[T1] Peter Selinger.
A short introduction to
the Lambda Calculus.
[T2] John C. Mitchell.
Foundations for Programming Languages.
The MIT press, 1996.
[T3] JeanYves Girard, Y. Lafont, P. Taylor.
Proofs and Types.
Cambridge University Press, 1989.
[T4] Robert Harper.
Practical Foundations for Programming Languages.
Working draft, 2010.
[T5] Benjamin C. Pierce.
Types and Programming Languages.
The MIT press, 2002.
[T6] Benjamin C. Pierce.
Basic Category Theory for Computer Scientists.
The MIT press, 1991.
Functional programming
[FP1]Miran Lipovača.
Learn You a Haskell for Great Good. 2011.
[FP2]Chris Okasaki.
Purely Functional Data Structure.
[FP3]Richard Bird.
Pearls of Functional Algorithm Design.
Cambridge University Design, 2010.
[FP4]Bryan O'Sullivan, Don Stewart, and John Goerzen.
Real World Haskell. O'Reilly, 2008.
[FP5]Didier Rémy.
Using, Understanding, and Unraveling The OCaml Language.
Course schedule
Date

Content

Lecture notes

Sept. 14

Lambdacalculus: syntax, reduction, normalization, confluency, expresiveness, ...
Ref: [T1] (chapter 14)

Slides

Sept. 21

Typed lambda calculi and PCF
Ref:
[T1] (chapter 11), [T2] (chapter 2), [T3] (chapter 4, 6, 7)

Slides:
I: Types
II: PCF

Sept. 28 Sept. 29

FPL: introduction to Haskell (evaluation, recursion schemes, data types, pattern matching, type classes, ...)
Ref: [FP1] (chapter 18)

Sample code

Oct. 12

Type inference
Ref:
[T1] (Chapter 9), [T2] (chapter 11)

Slides

Oct. 19

PCF: operational and denotational semantics
Ref:
[T1] (Chapter 10, 11, 12), [T2] (Chapter 2, 4, 5)

Slides

Oct. 26

Imperative languages and monad
Ref:
[T2] (Chapter 6)
N. Benton, J. Hughes, E. Moggi. Monads and effects.
E. Moggi. An abstract view of programming languages.
E. Moggi. Notions of computations and monads.

Slides

Nov. 2

Advanced type systems (System F, recursive types)
Ref:
[T3] (chapter 11), [T4] (part VIII, part VI)

slides

Oct. 26 Nov. 2

FPL: advanced haskell programming (monad, concurrent programming, functional data structure, ...)
Ref:
E. Söylemez. Understanding Haskell Monads.
S. Marlow. Parallel and concurrent programming in Haskell.


Nov.9 Nov. 16

Advanced topics in type theory
Ref:
[T6] Chapter 1 and 2 for category theory


