582655: Formal Type Theory (4 cr), autumn 2009

News

2010-05-18: The Spring 2010 Coq project assignment and its sample solution are now available.
2010-04-08: The questions and sample solutions to the March 26th separate exam are now available.
2010-01-10: The results are in. See the final version of the checklist for details of the exercise points. Those who failed, or wish to raise their grade, can either take a Coq project to replace the exercise points, or retake the exam to replace the exam points, or both. See the details for retaking and separate exams.
2009-12-16: The exam with sample solutions is now posted.
2009-12-13: The solutions to the fifth exercises are up. Also, the checklist has been updated.
2009-12-10: Some words on the exam. The Ott files for the last lectures are also up.
2009-12-05: Solutions to the fourth exercise now up.
2009-12-04: Fifth exercise now up.
2009-12-03: The Ott definitions discussed during today's lecture have been added. Note also that you can post requests about the contents of the last lecture in the newsgroup. Also, there is a checklist for the points from the first two exercises. Check it to verify that your submissions have been received. The department's spam filter has been notoriously eager to classify exercise submissions as spam.
2009-12-02: The eighth lecture notes have been revised. Also, the PDF version of the notes now includes the language definitions.
2009-12-01: Ninth lecture added.
2009-11-28: Fourth exercise added. NOTE: the policy for late returns has changed.
2009-11-26: Seventh and eighth lecture added
2009-11-21: Third exercise and the solutions to the second ones added
2009-11-20: Sixth lecture added
2009-11-17: Fifth lecture added
2009-11-13: Second exercise and the solutions to the first ones added
2009-11-10: Third lecture added
2009-11-05: Second lecture and first exercise added
2009-11-04: There's a newsgroup!
2009-11-03: First lecture is up (now in several formats)
2009-11-02: A new page about the software used during the course

News
Overview
Schedule
Lectures
Exercises
Exam
Newsgroup
Passing the course
Prerequisites and related courses
Software
Literature
Preliminary course outline
Links

Overview

The course covers basic concepts of programming language theory: formal languages, operational semantics and type systems. A central concept is the notion of type safety: we prove that if a program is well-typed (and the type system is good), then its execution is guaranteed to be free from (certain kinds of) errors.

The course is also an exercise in rigorously formal definitions and proof techniques. To enforce rigor, we use the Coq proof assistant. In addition to being a practical proof tool, Coq also provides an extremely sophisticated type system which illustrates another tangent to the core subject matter: the Curry-Howard correspondence between programming languages and logic.

Schedule

Lectures

Lauri Alanko, Nov 3rd to Dec 10th, Tuesdays and Thursdays 12-14, B222

Recitations and exercise advice

Joel Kaasinen, Nov 5th to Dec 10th, Thursdays at B221. Exact time varies:

Nov 5th: 14-18
Nov 12th: 14-16 (Lauri is substituting)
Nov 19th to Dec 10th: 14-17

Final exam

Monday Dec 14th, 16-19, A111.

Lectures

The lecture notes are available in several formats. The best way to study them is to load the source code into Proof General (or CoqIDE). The source is available here. On the Department's systems, they are also directly installed in /home/group/formal/ftt09/.

The notes are also available as HTML files, which are easy to access quickly. Finally, for off-line reading, the notes are also available as a single PDF file here. The file will be updated as new material gets added.

Nov 3rd

Introduction, basic functional programming.

Slides: lecture1.pdf
References:
- Java is not type-safe (Saraswat 1997)
- Generic Java type inference is unsound (Jeffrey 2001)
- Fully Reflexive Intensional Type Analysis (Saha, Trifonov, Shao 2000)
Lecture notes: natbool.v, natbool.html
Supplementary material: Basics at UPenn. (Up to and including numbers, ignoring the proofs.)

Nov 5th

Polymorphism, logic, equality.

Lecture notes: poly.v, poly.html, logic.v, logic.html
Supplementary material at UPenn: Poly and Logic

Nov 10th

Tactics: introductions, rewriting, cases

Lecture notes: tactics.v, tactics.html. In addition, util.v is also needed to make the custom tactics available.
Supplementary material: Basics (the proof bits)

Nov 12th

Relations, lists, more induction

No lecture notes, reviewed some of the SF material: Basics (intros, destruct and induction), Lists, Logic (relations)
Reading: TAPL Chapter 2

Nov 17th

Abstract syntax, operational semantics, booleans and numbers

Lecture notes: tapl_ch3.v, tapl_ch3.html, bool.ott, nat.ott, common.ott, untyped_bool_lang.v, untyped_arith_lang.v.
Reading: TAPL Chapter 3
Supplementary material: Smallstep

Nov 19th

Operational semantics continued, types for arithmetic.

Lecture notes: tapl_ch8.v, tapl_ch8.html, untyped_arith_lang.v. See in the source directory to find the Ott files that were used to generate the language definitions.
Reading: TAPL Chapter 8
Supplementary material: Stlc (part "Typed arithmetic expressions")

Nov 24th

Typed lambda calculus

Lecture notes: tapl_ch9.v, tapl_ch9.html, typed_bool_fun_lang.v
Reading: TAPL Chapter 9 (and 5.1 and 5.3 for background)
Supplementary material: Stlc (later parts)

Nov 26th

Type preservation, normalization

Lecture notes: tapl_ch12.v, tapl_ch12.html, typed_base_fun_lang.v
Reading: TAPL Chapter 12

Dec 1st

Normalization continued, general recursion

Lecture notes (preliminary): tapl_ch11.v, typed_arith_fix_lang.v
Reading: TAPL 11.11

Dec 3rd

Simple extensions

Ott files for the extensions discussed: fix.ott, pair.ott, record.ott, sum.ott, variant.ott, also let.ott (not discussed). If you dare, you can also look at the generated Coq formalization, which becomes rather messy in the presence of records and variants: typed_misc_lang.v.
Reading: TAPL Chapter 11
Supplementary material: MoreStlc

Dec 8th

References

Ott files for references: unit.ott, store.ott, fun_store.ott, ref.ott.
Reading: TAPL Chapter 13

Dec 10th

Exam overview, general Q & A, exceptions and effect systems.

Ott files: exc.ott, effect.ott, exc_effect.ott, ref_effect.ott.

Homework exercises

The homework exercises can be solved either alone or in groups of two. That is, you may have one partner (who is also on the course) with whom you may collaborate fully when solving the exercises. If doing the exercises with a partner, return just a single solution jointly, with the names of both members of the group in the submission.

The solutions should be sent as e-mail attachments to ftt09@cs.helsinki.fi. For every starting four hours after the deadline, the maximum number of points awarded for the exercises decreases by one, until 24 hours have passed, at which point no further returns are accepted.

In the exercise files there is some space reserved for comments. Feel free to comment on the difficulty, workload, or fun factor of the exercises. The comments will not affect grading.

First exercises: ex1.v. Deadline on Thursday, November 12th, 8:00 AM. Sample solutions.
Second exercises: ex2.v. Deadline on Friday, November 20th, 3:00 AM. Sample solutions. You need to have to have the Software Foundations sources in Coq's include path. The individual files are here and the package as a tarball is here. Note that use of automation tactics like auto is not allowed with this week's exercises. Just use the tactics listed in the exercise file.
Third exercises: ex3.v. Deadline on Friday, November 27th, 3:00 AM. Sample solutions. Some of the problems use variant languages: wrong (ott, coq) and bigstep (ott, coq).
Fourth exercises: ex4.v. Deadline on Friday, December 4th, 3:00 AM. Sample solutions.
Fifth exercises: ex5.v. Deadline on Friday, December 11th, 3:00 AM. Sample solutions. For problem 4, see also paircase_grammar.ott and typed_paircase_lang.v.

Exam

For information about separate exams, see passing

The course exam was held on Monday Dec 14th, 16-19 at A111. The exam covers chapters 3, 8, 9, 11 and 12, and sections 13.1, 13.2 and 13.3 of TAPL, as well as all everything about Coq that has been discussed during the course. The exam with sample solutions is here.

Some classes of questions that may well appear in the exam:

"Express the following definition in Coq"
"Here is a proof context and a goal. Spell out the tactic(s) that solve the goal in the current context."
"Given the following evaluation rules, what does this term evaluate to in one step?"
"Does this term have a normal form? If it does, what is it?"
"Is the following typing judgement correct?"
"Suppose we change a language by adding/removing/changing a rule in the following fashion. Which properties of the language are lost, and which are preserved?"
"Prove informally the following proposition."
"Here is an informal description of a language feature. Design evaluation and typing rules that express its semantics correctly without breaking any of the desirable properties of the language."

You can look at old exams from CIS 500 at upenn to get some idea of what the exam may look like, even though those exams cover several things that we haven't discussed on this course.

Newsgroup

The recommended forum for course-related discussions is the newsgroup hy.opiskelu.tktl.symbo in the University's news server. There are a number of ways to access it:

If your browser supports news URLs, one of these links might work directly: nntp://news.helsinki.fi/hy.opiskelu.tktl.symbo or news://hy.opiskelu.tktl.symbo.
In the Department's computer systems, the newsgroups can be directly accessed with the following programs:
- thunderbird
- alpine
- slrn
- tin
- gnus (emacs package)
With the first two, first select the folder news.helsinki.fi. Then just subscribe to (or add) the group hy.opiskelu.tktl.symbo
You can also use those programs (or any other programs that support newsgroups) on other machines. Just make sure that news.helsinki.fi has been set as the NNTP server.

Please don't ask for, or give out, direct solutions to homework exercises, nor parts of them. The purpose of the newsgroup is to help promote understanding, not avoid it.

Passing the course

The course is passed by returning weekly exercises, and successfully participating in the final exam. Attending the lectures and recital sessions is voluntary.

After the lecture course, the course can be passed by completing a Coq project assignment and attending an exam that covers the same area as the exam for the lecture course. Alternatively, beginning from Summer 2010, the course can be passed by attending to an exam that covers the entirety of chapters 3, 5, 6, 8, 9, 11, 12, 13 and 14 of TAPL, including all the extra material discussed in the book's exercises and their solutions. In either case, the lecturer should be contacted before registering for the exam.

The next exams are:

Jan 26th 2010: Only for those who attended the course or are taking a Coq project
Mar 26th 2010: Same as previous. Questions and sample solutions are available.
Aug 10th 2010: Wider book exam, no Coq project necessary

Prerequisites and related courses

The course touches on several topics that have been treated more extensively on other courses. To avoid overlap, and due to time constraints, these are only skimmed during the course. It is possible to learn about these while the course is running, but it's a much better idea to at least get acquainted with these before the course begins.

Functional programming

Functional programming is pertinent to the course for two reasons. First, the examined calculi are purely functional (simply because we have no time to study imperative languages), and hence basic knowledge of functional programming is required to grasp how the calculi are relevant to real-world programming languages. Second, the Coq proof language itself is a functional language, and functional programming techniques are directly applicable as proof techniques.

From the Spring 2009 course Johdatus funktionaaliseen ohjelmointiin (in Finnish), the most relevant topics are higher order functions, inductive data types, pattern matching and structural recursion.

Lambda calculus

The Autumn 2008 course Johdatus lambda-kalkyyliin (in Finnish) introduced the untyped lambda calculus. Most relevant topics for the present course are the untyped lambda calculus itself, the reduction relation, and the intricacies of variable substitution.

Logic

This course is very much about logic in two ways: we use logic to formally prove properties of certain languages, and we study logic almost by accident, since the languages turn out to be directly related to intuitionistic propositional logic. From the course Logiikka I (in Finnish), at least natural deduction is essential background.

Software

The software required on the course has been installed on the Department's computer systems. See a separate page for a more detailed description on how to use it.

If you wish to install the software on a personal machine, you will need at least the latest released versions of Coq and Proof General. If you don't like Emacs, you can also use CoqIDE which comes with Coq, but if you do, you're on your own.

Literature

The primary textbook for the course is Types and Programming Languages by Benjamin C. Pierce. The Software Foundations material at UPenn serves as supplementary material, and gives an idea of what to expect from the current course.

Preliminary course outline

Introduction: languages, types and logic (TAPL Chapter 1)
Programming in Coq: functions, data types, pattern matching
Proving in Coq: tactics
Structural recursion and induction (TAPL Chapter 2)
Language definitions, operational semantics (TAPL Chapter 3)
Type systems, type safety (TAPL Chapter 8)
Simply typed lambda calculus (TAPL Chapter 9)
Extensions to STLC: unit, empty, pair and sum types, and general recursion (TAPL Chapter 10)
(Normalization of STLC (TAPL Chapter 12))
(Parametric polymorphism, System F (TAPL Chapter 23))

Department of Computer Science

Department information