Theory and Practice of Functional Programming

Lecture place: Room N408 of the GUCAS building, Zhongguancun.
Lecture time: Friday morning 8:00 -- 11:40

Lecturer: Dr. ZHANG Yu
yzhang AT ios DOT ac DOT cn
Office: ISCAS Building #5, Room 315      Phone: (010) 6266 1656
Office hour: Tuesday afternoon 15:00 -- 18:00

The course consists of two major parts:

Theory: fundamental theories of PL: lambda-calculus 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.


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.


[T1] Peter Selinger. A short introduction to the Lambda Calculus.

[T2] John C. Mitchell. Foundations for Programming Languages. The MIT press, 1996.

[T3] Jean-Yves 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 Lambda-calculus: syntax, reduction, normalization, confluency, expresiveness, ...
Ref: [T1] (chapter 1-4)
Sept. 21 Typed lambda calculi and PCF
[T1] (chapter 11), [T2] (chapter 2), [T3] (chapter 4, 6, 7)
I: Types
Sept. 28
Sept. 29
FPL: introduction to Haskell (evaluation, recursion schemes, data types, pattern matching, type classes, ...)
Ref: [FP1] (chapter 1-8)
Sample code
Oct. 12 Type inference
Ref: [T1] (Chapter 9), [T2] (chapter 11)
Oct. 19 PCF: operational and denotational semantics
Ref: [T1] (Chapter 10, 11, 12), [T2] (Chapter 2, 4, 5)
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.
Nov. 2 Advanced type systems (System F, recursive types)
[T3] (chapter 11), [T4] (part VIII, part VI)
Oct. 26
Nov. 2
FPL: advanced haskell programming (monad, concurrent programming, functional data structure, ...)
E. Söylemez. Understanding Haskell Monads.
S. Marlow. Parallel and concurrent programming in Haskell.
Nov. 16
Advanced topics in type theory
[T6] Chapter 1 and 2 for category theory

Copyright © ZHANG Yu. Laboratory of Computer Science, ISCAS, Beijing.