Instructor: Stephanie Weirich
Time: Mon/Wed 1:30-3:00
Location: Moore 212
Prerequisites: CIS 500 (Software Foundations) or permission of the instructor.
Office hours: M 3:00 in Levine 510 or by appointment

Schedule

Semester Project Ideas [upenn.edu access only]

ATTAPL Errata

Course Description

Textbooks

• Benjamin Pierce. Types and Programming Languages (TAPL).
• Benjamin Pierce, ed. Advanced Topics in Types and Programming
  Languages (ATTAPL). (Prepublication, chapters will be provided. You can also email Benjamin Pierce for a current draft. )

This course delves into the state of the art of type systems and
programming languages. During the semester, we will cover three
sections of a new textbook on advanced type systems.

First we will discuss how type systems can be used to reason about
programs. We can use the type system of a programming language to
structure proofs about that language (such as the correctness of an
equivalence algorithm) or proofs about programs written in that
language (such as contextual equivalence of two programs).

Next, we look at how type systems can be made more precise. In other
words, how can we define them so that type soundness implies stronger
properties about well-typed programs? Dependent type systems
incorporate terms into the type system, so that types can be more
descriptive. For example, by including the number of elements in the
type of an array we can statically ensure that array accesses are
within bounds.

Effect type systems allow types to describe properties of
computation. For example, the type of a function in an effect system
could (approximately) describe the exceptions that it might raises,
the time that it takes to execute, or what sections of memory that it
accesses. A particularly important form of effect system is
region-based memory management that uses effect inference to
statically determine when memory should be allocated or deallocated by
the program.

Substructural type systems augment type mechanisms with the ability to
control the number and order of uses of a data structure or
operation. They are particularly useful for constraining interfaces
that provide access to system resources such as files, locks and
memory.

Finally, we will study type mechanisms designed for programming in the
large. In particular, we will look at the design of module systems,
from the simplest containing only basic mechanisms such as namespace
management and inter-module type checking to the most advanced that
extend even the sophisticated module systems of the ML language.

Tentative list of topics

• Foundations
  • Polymorphic Lambda Calculus (TAPL 23,24,30)
  • Recursive types (TAPL 20,21)
• Reasoning about programs (ATTAPL II)
  • Logical relations
  • Typed operational reasoning
• Precise type analysis (ATTAPL III)
  • Dependent types
  • Effect and region types
  • Substructural types
• Programming in the large (ATTAPL V)
  • Advanced module systems
  • Type definitions

Students will be expected to bring questions based on the current reading to each class and participate in discussion. The majority of the course grade will come from the semester project.

Project Information

The goal of the course project is to produce a research paper suitable for publication in a workshop or conference forum. Students are to work together in small groups (2 or 3 people).

Rough Timeline

• Form groups and choose topic by second Sept 10.
• Submit a ~2 page writeup of related work by Oct 1.
• Submit a description of technical material of the project by Nov 24.
• Submit the completed project paper, including introduction, motivation, summary and contributions by the end of the semester.
• Presentations given in the last week of class.

Grading criteria

The projects will be graded based on the writeup at each phase, the quality of the project technically, and the resulting final paper. Writeups are expected to require revision and editing throughout the semester; feedback on writing style and content will be provided. Furthermore, each group will be encouraged to peer review the other groups' submissions at each step of the project.