|
Semantics of Programming Languages Course #: COMP 411 |
|
|
|
|
As computer programs play an increasingly more significant role in our daily lives, knowing what they are supposed to be doing and its relation what they actually do becomes particularly important. For example, given two programs we might want ask: are they equivalent? If we optimize, compile, or even write programs, this fundamental question comes up. Often, we rely on intuition for answering this question. But in critical applications where avoiding programming errors is important, or if we just want to produce higher quality software, there is a need for more rigorous techniques to answer this question. The idea is that the less we rely on intuition and replace by analytical methods, the more reliable the resulting software systems can be. The goal of this course is to introduce you to some mathematical tools that can help you to do this. Collectively, they are called formal semantics.
The course will focus on operational semantics and type systems. These tools will be applied to a wide range of programming languages, including imperative, non-deterministic, parallel (or concurrent), as well as functional programming languages. Features such as strictness, laziness, recursion and recursive datatypes will also be covered. The course will follow closely the textbook Types and Programming Languages by Benjamin Pierce.
Course work will include reading the text book, solving homework problems (40%), a midterm (20%), and a final (30%). Homework problems are assigned each Monday, cover material up to Wedensday, and are due by Friday. Timeliness, attendance and preparedness for class are required and are evaluated by quizes (10%). Homeworks must be submitted as plain text, by email, and before class on the due date. Late submissions are not accepted except in extraordinary circumstances, and must be by arranged before the original deadline.
|
# |
Date |
Day |
Topic |
Homework |
Comments |
|
1 |
1/12 |
M |
Organization.
Introduction to types and programming languages (Ch 1) |
2.2.{6,7,8}.
Download and install OCaml. Implement factorial, Fibonacci, and Ackermann,
and hand them in. |
|
|
2 |
1/14 |
W |
Mathematical preliminaries
(Ch 2) |
|
|
|
3 |
1/16 |
F |
Untyped arithmetic expressions (Ch 3) |
|
|
|
|
1/19 |
M |
No class today (MLK) |
3.2.{5,6}.
3.5.{10,13}. Read Ch 4. Download arith. Hand in a list of the types of
data-structures and functions used in the code. 4.2.2. |
|
|
4 |
1/21 |
W |
|
|
|
|
5 |
1/23 |
F |
(Ch 3 cont'd) |
|
|
|
6 |
1/26 |
M |
The untyped lambda calculus (Ch 5) |
5.2.{4,10} |
|
|
7 |
1/28 |
W |
Nameless representations of terms (Ch 6) and an implementation of the lambda calculus (Ch 7) |
|
|
|
8 |
1/30 |
F |
Typed arithmetic expressions (Ch 8) |
|
|
|
9 |
2/2 |
M |
Simply typed lambda calculus (Ch 9) |
8.2.3,8.3.{5,6,7,8},9.2.3,9.3.2,9.3.10,9.4.1. Test implementation in Ch 10 using a set of 10 different examples, and hand in output. |
|
|
10 |
2/4 |
W |
An implementation of simple types (Ch 10) |
|
|
|
11 |
2/6 |
F |
Some simple extensions to simple types (Ch 11.[1-7]) |
|
|
|
12 |
2/9 |
M |
More extensions to simple types (Ch 11.[8-12]) |
11.5.1, 11.8.2, 11.9.1, 11.11.{1,2}, 11.12.1 |
|
|
13 |
2/11 |
W |
Normalization (Ch 12) |
|
|
|
14 |
2/13 |
F |
Adding references to the simply typed lambda calculus (Ch 13) |
|
|
|
15 |
2/16 |
M |
Adding exceptions (Ch 14) |
|
|
|
16 |
2/18 |
W |
Subtyping basics (Ch 15.[1-4]) |
|
|
|
17 |
2/20 |
F |
Subtyping and interaction with other features (Ch 15.[5-8]) |
|
|
|
18 |
2/23 |
M |
Some metatheoretic properties of subtyping (Ch 16) |
12.1.{4,5,7} |
|
|
19 |
2/25 |
W |
An implementation of subtyping (Ch 17) |
|
|
|
20 |
2/27 |
F |
|
|
|
|
|
3/1 |
M |
|
|
|
|
|
3/3 |
W |
|
|
|
|
|
3/5 |
F |
|
|
|
| 21 | 3/8 | M | Imperative objects (Ch 18.[1-6]) |
16.2.{1,3,5,6}, 16.3.{2,3,4}, 16.4.1, 17.3.{1,2,3,4} | |
| 22 | 3/11 | W | Imperative objects (Ch 18.[6-14]) |
||
|
23 |
3/13 |
F |
Featherweight Java (Ch 19) |
||
|
24 |
3/15 |
M |
|
No homework this week |
|
|
25 |
3/17 |
W |
|
|
|
|
26 |
3/19 |
F |
|
|
|
|
27 |
3/22 |
M |
Metatheoretic properties of recursive types (Ch 21) |
No homework this week |
|
|
28 |
3/24 |
W |
Polymorphism and type reconstruction (Ch 22) |
|
|
|
29 |
3/26 |
F |
Universal types basics (Ch 23.[1-6]) |
|
|
|
30 |
3/29 |
M |
Universal types, erasure, parametricity, and impredicativity (Ch 23.[7-11]) |
No homework this week
|
|
|
31 |
3/31 |
W |
Existential types (Ch 24) |
|
|
|
32 |
4/2 |
F |
An implementation of system F (Ch 25) |
|
|
|
33 |
4/5 |
M |
Bounded quantification basics (Ch 26.[1-4]) |
22.3.{9,10,11}, 22.4.{3,6} |
|
|
34 |
4/7 |
W |
Bounded quantification and existential types (Ch 26.{5,6}) and implementation (Ch 27) |
|
|
|
35 |
4/9 |
F |
Metatheoretic properties of bounded quantification (Ch 28) |
|
|
|
36 |
4/12 |
M |
Higher-order polymorphism (Ch 29, Ch 30.[1-3]) |
23.4.{3,5,6,8,9}, 23.5.{1,2} |
|
|
37 |
4/14 |
W |
Fragments of F-omega, and dependent types (Ch 30.{4,5}) |
|
|
|
38 |
4/16 |
F |
Higher-order subtyping (Ch 31) |
|
|
|
39 |
4/19 |
M |
Purely functional objects (Ch 32) |
TBA |
|
|
40 |
4/21 |
W |
|
||
|
41 |
4/23 |
F |
|
Students with disabilities are encouraged to contact me during the first two weeks of class regarding any special needs. Students with disabilities should also contact Disabled Student Services in the Ley Student Center and the Rice Disability Support Services.