|
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 cover techniques such as operational, denotational, and axiomatic
semantics, as well as 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 The
Formal Semantics of Programming Languages by Glynn Winskel. (A list of errata
is available online).
Course
work will include reading the text book (about 9 pages per lecture), solving
basic homework problems, and a term project. Homework problems will be assigned each class, and will be
due by next class. Many of these
problems will consist of writing out more detailed solutions to problems solved
in the book. The term project will
involve defining the semantics of a cut-down language of your choosing, and
establishing basic properties of this semantics.
The final project is intended to give you hands on experience with the material taught in the course and also to allow you to explore in more depth a topic of your own interest. Acceptable projects can be a programming project, a survey of recent research on some relevant topic, or a small research paper. Everybody must select a project and write a very short (one to two pages) proposal arguing what is expected to be learned from the project (why is it interesting to you) and giving a work schedule. Make sure to budget time for writing a short paper describing the project and for preparing a short (10-15 minute) presentation during the last week of classes. Projects can be individual or in small groups. The due dates for the project proposal and for the final presentation will be announced later.
Students are encouraged to discuss the material covered in class and in assignments on the news group rice.owlnews.comp411.
|
# |
Date |
Day |
Topic |
Reading (Before class) |
Excercises (Due next class) |
|
1 |
1/13 |
M |
Organizational Meeting |
|
|
|
2 |
1/15 |
W |
Basic set theory |
1.1-1.4 |
1.1-1.8 |
|
3 |
1/17 |
F |
Operational Semantics |
2.1-2.4 |
2.1-2.7 |
|
4 |
1/22 |
W |
|
2.5-3.2 |
2.8-2.11,
3.1-3.6 |
|
5 |
1/24 |
F |
Induction |
3.3-3.6 |
3.7-3.13 |
|
6 |
1/27 |
M |
Inductive definitions |
4.1-4.3.3 |
4.1-4.8 |
|
7 |
1/29 |
W |
|
4.4-5.1 |
4.9-4.14 |
|
8 |
1/31 |
F |
Denotational semantics |
5.2-5.3 |
5.1-5.9 |
|
9 |
2/3 |
M |
|
5.4 |
5.10-5.13 |
|
10 |
2/5 |
W |
|
5.5 |
5.14 |
|
11 |
2/7 |
F |
Axiomatic semantics |
6.1-6.2 |
6.1-6.6 |
|
12 |
2/10 |
M |
|
6.3-6.5 |
6.7-6.12 |
|
13 |
2/12 |
W |
|
6.6-7.1 |
6.13-6.17 |
|
14 |
2/14 |
F |
Completeness of axiomatic semantics |
7.2 |
7.1-7.8 |
|
15 |
2/17 |
M |
|
7.3-7.5 |
7.9-7.15 |
|
16 |
2/19 |
W |
Domain theory |
8.1-8.3.2 |
8.1-8.7 |
|
17 |
2/21 |
F |
|
8.3.3-8.3.4 |
8.8-8.15 |
|
18 |
2/24 |
M |
|
8.4-9.1 |
8.16-9.1 |
|
19 |
2/26 |
W |
Recursion equations |
9.2-9.4 |
9.2-9.8 |
|
20 |
2/28 |
F |
|
9.5-9.7 |
9.9-9.16 |
|
21 |
3/3 |
M |
|
9.8-10.1 |
10.1-10.3 |
|
22 |
3/5 |
W |
Techniques for recursion |
10.2 |
10.4-10.14 |
|
23 |
3/7 |
F |
|
10.3-10.6 |
10.15-10.20 |
|
24 |
3/17 |
M |
Higher-order types (“functions”) |
11.1-11.4 |
11.1-11.13 |
|
25 |
3/19 |
W |
|
11.4-11.6 |
11.14-11.6 |
|
26 |
3/21 |
F |
|
11.7-11.8 |
11.7-11.24 |
|
27 |
3/24 |
M |
|
11.9-11.10 |
11.25-11.28 |
|
28 |
3/26 |
W |
|
11.11-12.2 |
11.29-12.4 |
|
29 |
3/28 |
F |
Information systems |
12.3-12.4 |
12.5-12.16 |
|
30 |
3/31 |
M |
|
12.5-12.5.3 |
12.17-12.28 |
|
31 |
4/2 |
W |
|
12.5.4-12.6 |
12.29-12.34 |
|
32 |
4/4 |
F |
Recursive types (“data-types”) |
13.1-13.3 |
13.1-13.3 |
|
33 |
4/7 |
M |
|
13.4 |
13.4-13.10 |
|
34 |
4/9 |
W |
|
13.5 |
13.11-13.20 |
|
35 |
4/11 |
F |
|
13.6-13.8 |
13.21-13.25 |
|
36 |
4/14 |
M |
|
13.9-13.11 |
13.26-13.37 |
|
37 |
4/16 |
W |
Parallelism |
14.1-14.2 |
14.1-14.4 |
|
38 |
4/18 |
F |
|
14.3-14.4 |
|
|
39 |
4/21 |
M |
|
14.5-14.6 |
14.5-14.9 |
|
40 |
4/23 |
W |
|
14.7-14.9 |
14.10-14.23 |
|
41 |
4/25 |
F |
|
|
|
1. Ocaml textbook draft
·
TBA
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.