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. 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] 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) 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 1-8) 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