Advanced Functional Programming Seminar Course

About the Course

This seminar course focuses on the principles and practice of purely functional programming. The course features the CakeML language and the Ott tool for defining languages and inductive relations.

Seminar Slides

Seminar	Topic	Slides and other resources
1	Functional languages, abstract syntax trees, variable binding, and inductive definitions	slides PFPL chapters 1 and 2 introduction to inductive definitions small functional language Ott file small functional language pdf
2	Untyped lambda calculus, operational semantics, combinators, encodings	slides supplement by Harper lambda calculus Ott file lambda calculus pdf
3	Simply typed lambda calculus and beyond (OCaml Light, CakeML)	slides PFPL chapter 4 simply typed lambda calculus Ott file simply typed lambda calculus pdf simply typed lambda calculus with Booleans Ott file simply typed lambda calculus with Booleans pdf Definition of STLC in Software Foundations book by Pierce et al. Properties of STLC in Software Foundations book by Pierce et al. Research paper on OCaml Light Full definition of OCaml Light, see also the Ott repository Research paper on the CakeML type system Example CakeML program (proof checker for propositional logic proofs)
4	Data types	slides PFPL chapters 9, 10, 11 binary products Ott file binary products pdf general products Ott file general products pdf simply typed lambda calculus with natural numbers Ott file simply typed lambda calculus with natural numbers pdf
5	From primitive to general recursion	slides PFPL chapters 15, 19, 20
6	Proofs of function properties by structural induction	slides Note on structural induction by Michael Erdmann some structural induction proofs on lists Research paper from 1968 on structural induction by Ron Burstall
7	Function property specification and contracts	slides PFPL chapter 16, for theoretical background on parametric polymorphism and type variables Why3 - Where Programs Meet Provers by Filliatre and Paskevich, overview of the WhyML language and toolchain Why3 website with gallery of verified WhyML programs WhyML function with specification for the GCD function. WhyML functions with specifications for list reversal WhyML functions with specifications for list-based sets
8	Abstract types	slides PFPL chapter 17 On Understanding Data Abstraction, Revisited, voluntary reading on connections to object orientation Queue abstract datatype in CakeML, tested with version CakeML v2184
9	Module types and typeclasses	slides PFPL chapter 44 Standard ML Basis library OCaml Stdlib
10	Purely functional data structures, I	slides Purely functional data structures book, chapters 3 and 5 Okasaki's PhD thesis, contains subset of content in the book
11	Purely functional data structures, II	slides Purely functional data structures book, chapters 9 and 10 Okasaki's PhD thesis, contains subset of content in the book
12	Research paper presentations	Presented papers: How to Make Ad-hoc Polymorphism Less Ad Hoc Modular Type Classes A theory of type polymorphism in programming Verified Compilation and Optimization of Floating-Point Programs in CakeML Red-black trees in a functional setting
13	Advanced topics: Church's simple types & dependent types	slides Church's simple type theory in Stanford's encyclopedia of philosophy Thorsten Altenkirch's lecture notes on dependent types Intuitionistic type theory in Stanford's encyclopedia of philosophy
14	Tool and language demonstrations

Homeworks

Related Research Papers

MacQueen, David B. Using Dependent Types to Express Modular Structure. POPL '86, pp. 277-286. [Paper about ML module system]
Wadler, P. and Blott, S. How to Make Ad-hoc Polymorphism Less Ad Hoc. POPL '89, pp. 60-76. [Paper about typeclasses]
Dreyer, Derek and Harper, Robert and Chakravarty, Manuel M. T. and Keller, Gabriele. Modular Type Classes. POPL '07, pp. 63-70. [Paper about connections between typeclasses and module systems]
Becker et al. Verified Compilation and Optimization of Floating-Point Programs in CakeML. ECOOP '22, pp. 1:1–1:12. [Paper about floating points in a functional language]
Harper, Robert. Proof-directed Debugging. Journal of Functional Programming, 9:4, pp. 463-469. [Paper about purely functional regular expression matcher using closures]
Meijer, Erik and Fokkinga, Maarten and Patterson, Ross. Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. FPCA 1991. [Applying category-theoretic concepts in functional programming]
Leroy, Xavier. Manifest types, modules, and separate compilation. POPL 1994. [Module systems and how they enable incremental source compilation]
Okasaki, Chris. Red-black trees in a functional setting. Journal of Functional Programming, 1999.
Milner, Robin. A theory of type polymorphism in programming. JCSS, 1978.

Resources

Practical Foundations of Programming Languages (main course book, abbreviated pdf)
Ott tool for defining languages and inductive relations