15-814: Fall 2003: Introduction to Type Systems

Time: TR 1:30pm — 2:50pm
Location: Wean Hall 5409
Instructor: Karl Crary
Instructor Office Hours: by appointment
TA: Aleksey Kliger
TA Office Hours: after lecture outside 5409 or in 8114; or by appointment.

Course Description

The course studies the theory of type systems, with a focus on applications of type systems to practical programming languages. The emphasis is on the mathematical foundations underlying type systems and operational semantics. The course includes a broad survey of the components that make up existing type systems, and also teaches the methodology behind the design of new type systems.

Book, Course Software

We are using Benjamin Pierce's Types and Programming Languages (errata) (Amazon), available in the CMU Bookstore.

The programming language used for projects in the course is Standard ML, using the SML/NJ implementation. You may wish to review the slides from our Introduction to SML. For further information, you may want to read Bob Harper's Programming in Standard ML, as well as the documentation for the SML'97 Basis Library.

A stable version of SML/NJ may be installed on facilitized machines using the misc collections. If you wish to install a copy of the software on your own (non-facilitized) machine, please install 110.0.7. Note that in the latest SML/NJ working version (110.43), the Compilation Manager (CM) underwent a redesign. As a result, there might be incompatabilities in later programming assignments between 110.0.7 and 110.43.

Homework policy

Both written and programming assignments are due at the beginning of lecture on the due date. Programming assignments must be copied to the submission directory, while written assignments will be collected in class.

Final exam

The final exam will be a 24 hour take-home exam. You may start at any time during the first week of finals. You may pick up the exam from Karl. If you're planning on picking it up outside of regular business hours, please make arrangements in advance by email.

If you plan on returning the exam over the weekend, you should return it by email. Otherwise hand the exam back to Karl within 24 hours.

Homework 6

  1. 15.2.5
  2. 15.3.6
  3. 26.2.2
  4. Let Counter = ∃α. α×(α→Nat)×(α→α). Let c1 = {*Nat, <1, λx:Nat.x, λx:Nat.succ x>} as Counter, and c2 = {*Nat×Nat, < <1,0>, λx:Nat×Nat. x.1 + x.2, λx:Nat×Nat. <succ x.2, x.1> >} as Counter. Show that c1 ≈ c2 : Counter
  5. Suppose f : ∀α. α→α→α, and v1 : T and v2 : T. Show that if f [T] v1 v2 →* v then either v = v1 or v = v2. (Hint: recall the example for f: ∀α. α→α from class)
  6. Extra credit: 26.3.5

Course Schedule

Date Topic Chapters Homework
4Syntax & Semantics2,3,4
9Operational Semantics; λ-calculus5,6,7Hw#1, due 9/16: 3.5.17, Port Chapter 4 to SML. Recommended: 3.5.16
11(cont'd) (encoding booleans in the λ-calculus)
16(cont'd) (encoding natural numbers, recursion)
18(cont'd) (substitution); Types & Type Safety8Hw#2, due 10/2: 5.2.8, 6.2.8, 7.3.1 (programming assignment), 6.1.1, 6.2.2, 6.2.5. Recommended: 6.2.7, 6.3.1
23(cont'd) (Safety, Progress, Canonical Forms, Preservation for typed Arith)
25Simply-typed λ-calculus9,10
10/2Expressions & Derived Forms11Hw#3, due 10/16: 8.3.6, 9.2.2, 9.3.2, 9.3.9 extended with products (show just the lambda and application, and pairing and projection cases of the proof), 9.3.10, Port Chapter 10 extended with nats and unit to SML
9Recursive types20, except 20.3
14(cont'd); References13
16(cont'd)Hw#4, due 10/30: see above.
30(cont'd)Hw#5, due 11/13: 13.5.2, preservation thm for refs (incl relevant store lemmas), 23.4.9, 23.4.10, 23.4.12, 23.5.2
11/4Existential types24,25
11Subtyping15, except 15.6
18Bounded Quantification26Hw#6 out (see above). Due 12/4
20(no class)
25Curry-Howard Isomorphism[handout]
12/2Substructural logics[paper]
12/4(cont'd)Homework 6 solution available: .ps, .pdf



The latter paper is worth reading at least for the fable in the introduction.

Linear Logic

$Log:	index.html,v $
# Revision 1.17  2003/11/19  15:36:35  aleksey
# I made a typo.  Problem set #6 includes problem 15.3.6, not 25.3.6
# Revision 1.16  2003/11/18  15:24:26  aleksey
# Hw 6 is up.  Also, info about final exam.
# Revision 1.15  2003/10/30  22:28:27  aleksey
# hw5 is up
# Revision 1.14  2003/10/27  16:55:13  aleksey
# revised schedule
Valid CSS! validate CSS
Valid XHTML 1.0! validate XHTML