Semantics of Programming Languages

Course #:  COMP 411
Instructor:  Walid Taha (DH 3103)
Class time:  MWF 10:00AM – 10:50AM (Office Hours:  M 2:00PM – 2:50PM)
Class room: TBA

 

 

 

Introduction

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.

Lectures

#

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

 

 

 

 

Additional References

1.      Ocaml textbook draft

Class Projects

        TBA

Accomodations for Students with Special Needs

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.