(Old announcements).

1. Pi-calculus. The pi-calculus is a prototypical programming language for concurrent processes invented by Milner, Parrow, and Walker in the late 1980's. Unlike lambda-calculus, it is not confluent; the behavior of a process is explicitly allowed to be non-deterministic. The presentation will explain the basics of pi-calculus, and show how lambda calculus can be simulated in pi-calculus. Reference: Robin Milner, Joachim Parrow, David Walker, "A Calculus of Mobile Processes, Part I", 1989.
2. HOL Light, a proof assistant based on lambda calculus. HOL Light is a software for writing mathematical definitions, theorems, and proofs in such a way that the proofs are machine-checkable. It is designed in two parts: a small trusted kernel for verifying theorems, together with programming facilities and a large library for generating proofs. The presentation will discuss the basic design of HOL and give some examples. Reference: John Harrison, "HOL Light Tutorial", 2006.
3. Domain theory and the D-infty construction. Domains are certain partially ordered sets that can be used as the interpretations of data types. Unlike with sets, it is possible to find a domain D such that the function space D->D is isomorphic to D. This way one can construct a model of the untyped lambda calculus. Reference: Samson Abramsky and Achim Jung, "Domain Theory", 1994, chapters 2, 3, and 5.
4. The language PCF. PCF stands for "programming with computable functions". The language PCF is an extension of simply-typed lambda calculus with booleans, natural numbers, and recursion. This project will present PCF as a case study to discuss semantics (operational and denotational) and the concepts of soundness, adequacy, and full abstraction. Reference: Carl A. Gunter, "Semantics of Programming Languages", MIT Press, 1992, chapters 4+6.
5. Type inference. Type inference is the process of finding the most general type, if any, of a term. It is a useful tool, as it allows programmers to write untyped programs and leave the typing to the compiler. This project presents the type inference algorithm for the simply-typed lambda calculus, and also for a version of polymorphism known as "ML-polymorphism". (There is no type inference algorithm for System F). References: Luis Damas and Robin Milner, "Principal type-schemes for functional programs", POPL 1982. Carl A. Gunter, "Semantics of Programming Languages", MIT Press, 1992, chapter 7.5.
6. System F and second-order arithmetic. An integer function is representable in System F if and only if it is provably total in second-order arithmetic. This presentation introduces the necessary terminology and gives an overview of the result. Reference: Jean-Yves Girard, Yves Lafont, and Paul Taylor, "Proofs and Types", Cambridge University Press, 1989, chapter 15.
7. Krivine's abstract machine. An abstract machine is a pencil-and-paper mechanism for running programs. It can serve as the basis for interpreters and compilers. Krivine's abstract machine uses a memory-and-stack architecture to evaluate lambda terms to head normal form. Reference: Ari Lamstein, "Theory and Implementation of a Functional Programming Language", Rose-Hulman Institute of Technology Undergraduate Mathematics Journal 1(2), 2000.

Problem Set 2, due Thursday, Oct 25.
Please do all exercises up to p.34 (except for Exercise 13, which was done in class).

Problem Set 3, due Tuesday, Nov 6 (firm deadline, please!).
Please do exercises 19-23.

All notes in a single file:

Individual Files:

Pages 17-20 (Programming in untyped lambda calculus) (posted Oct 1): [ps] [pdf].

Pages 21-28 (Church-Rosser) (posted Oct 9): [ps] [pdf].

Pages 29-34 (Church-Rosser) (posted Oct 11): [ps] [pdf].

Pages 35-38 (Combinatory algebras) (posted Oct 19): [ps] [pdf].

Pages 39-45 (Lambda algebras) (posted Oct 23, corrected Nov 5): [ps] [pdf].

Pages 46-53 (Simply-typed lambda calculus; natural deduction) (posted Oct 30): [ps] [pdf].

Pages 54-65 (Curry-Howard isomorphism; sums; classical logic) (posted Nov 5): [ps] [pdf].

Pages 66-94 (Polymorphism; strong normalization; models of simply-typed lambda calculus; PCF; complete partial orders) (posted Nov 21): [ps] [pdf].