Programming Languages and Types
Q3+4 2009, 10 ECTS
The invention of programming is maybe the most significant intellectual achievement of the 20th century. Nowadays, the beauty and elegance of programming is often hidden behind complex programming languages and large tool chains. This course will open your eyes and you will be trained to see the gold in the mud.
Content
The topics we will discuss include: names, definitional interpreters, lambda calculus, lazy evaluation, continuations, recursion, stateful vs. stateless, operational and denotational semantics, formal type systems and soundness, module systems, domain-specific languages, Scheme, Haskell, Scala, Java
Time and Place
Fridays from 9-12 in Shannon 157
Instructor
Schedule
The obligatory material is the basis for the exam. The advanced material exceeds what was discussed in class, but it is a good idea to take a look at it if you are striving for an A in the exam.
| Date | Topic | Obligatory Material | Advanced Material |
|---|---|---|---|
| January 30 | ASTs, parsing s-expressions substitution, first-order functions, scope environments vs substitution |
PLAI Chap. 1-5 Lectures Notes 1 2 3 |
Reynold's paper on definitional interpreters The next 700 programming languages |
| February 6 | No Lecture! | No Lecture! | No Lecture! |
| February 13 | First-class functions, closures, lazy evaluation
Introduction to Haskell Designing modular programs with lazy evaluation |
PLAI Chap. 6-7 Why functional programming matters Chap. 1-4 |
|
| February 20 | Implementation of lazy evaluation understanding and implementing recursion fixed-point operators Syntactic interpreter vs meta interpreter Co-data and Co-recursion |
PLAI Chap. 8-11 The Y combinator |
Slides on codata by T. Altenkirch Total Functional Programming |
| February 27 | State and Mutation | PLAI Chap. 12-14 | |
| March 6 |
Monads and effects modular interpreters/semantics |
Lecture Notes 1 2 3 The Essence of Functional Programming (except Chap. 3) Chap. 1+2 of Peyton-Jones' tutorial |
Monad Transformers Clean |
| March 13 | List Monad, IO Monad, Monad Composition Denotational Semantics |
Lecture Notes 1 2 | [Winskel] Chap. 8+12 Book by David Schmidt |
| April 3 | Denotational Semantics, ctd. Induction Principles Structural Operational Semantics | Lecture Notes 1 2 [Pierce] Chap. 3 |
On domain constructions: [Leeuwen] Chap. 12 ("Semantic Domains") |
| April 17 | Simply-Typed Lambda Calculus Type Soundness = Progress + Preservation Simple Extensions of STLC |
Lecture Notes 1 [Pierce] Chap. 8,9,11 |
|
| April 24 | Subtyping | Lecture Notes 1 [Pierce] Chap. 15,16 |
Structural Subtyping in OCaml |
| May 1 | Type Reconstruction System F Propositions-as-Types |
Lecture Notes 1 2 3 [Pierce] Chap. 22-23 |
Rank-n types in Haskell Wadler Twelf Coq |
| May 15 | Recursion and Continuations Guest Lecture by Olivier Danvy |
Notes/Exercise | |
| May 22 | Existential Types Higher-Order Types |
Lecture Notes 1 2 [Pierce] Chap. 24,29,30 |
|
| May 29 | Scala Case Study | Lecture Notes 1 | Case Study Existentials/HO types |
Hand-ins
Submit the hand-ins via the online system. The online system will not accept submissions after the deadline. One group will present their solution at the start of the lecture after the deadline. Each group will make exactly one such presentation during the course.
To get the point for your hand-in it is not necessary that all exercises are solved correctly, but if you failed then it should at least be obvious from your submission that you tried. Likewise, if you are awarded a point for your hand-in, then this does not imply that your solution is correct. All your questions about the hand-ins or your solution should be discussed during the presentation of the hand-in by one of the groups. You can of course always use the forum, too.
In the beginning, we will use PLT Scheme, together with the PLAI plug-in, whose installation is described here (see "Get the Software").
| Task | Hard Deadline | Presenter |
|---|---|---|
| Hand-in 1 | February 12, 23:59 | Group B |
| Hand-in 2 | February 12, 23:59 | Group C |
| Hand-in 3 | February 19, 23:59 | Group D |
| Hand-in 4 | February 26, 23:59 | Group E |
| Hand-in 5 | March 5, 23:59 | Group F |
| Hand-in 6 | March 12, 23:59 | Group G |
| Hand-in 7 | April 2, 23:59 | Group H |
| Hand-in 8 | April 16, 23:59 | Group I |
| Hand-in 9 | April 23, 23:59 | Group J |
| Hand-in 10 | April 30, 23:59 | Group K |
| Hand-in 11 | May 21, 23:59 | Group A |
| Hand-in 12 | May 28, 23:59 | Everyone |
Materials
We will mainly use the books by Krishnamurthi and Pierce.
 |
Shriram Krishnamurthi Programming Languages: Application and Interpretation Available online under Creative Commons License |
 |
Benjamin C. Pierce Types and Programming Languages MIT Press, 2002 |
- Glynn Winskel, The Formal Semantics of Programming Languages, MIT Press, 1993.
- J. van Leeuwen, Editor. Handbook of Theoretical Computer Science, Volume B, Elsevier, 1990.
- Wright and Felleisen, A Syntactic Approach to Type Soundness, Information and Computation 115, p.38-94, 1994 PS
Exam
There will be a multiple-choice exam on June 12, 2009, from 10-12, in IT-Huset Store Aud. To participate in the exam, you need to have 10 out of 13 possible points for your hand-ins. You can find some sample questions that give you an impression of the kinds of questions you can expect in the exam here.