Semantics of Programming Languages VT07
TDA345 - Semantik för programspråk (4,0 Poäng, ECTS 6,0) 0701 - DATAVETENSKAP DI CTH/GU
|
|
General
Lectures
- Overview of the lectures, and copies
of overheads.
Exercises
Assignments (Labs)
Examinations
|
Why Study Semantics?
Semantics in this context is the study of the principles and formal
(mathematical) techniques for the description of programming languages.
It provides the foundation
for reasoning about the reliability and correctness of programs and
computers themselves, and essential in the design of programming
languages and program manipulation tools such as translators,
compilers, optimizers, verifiers.
Who should Study Semantics?
You should have previously studied a course in programming languages (and
of course basic programmming skills are assumed). It is an advantage if you
have studied courses such as discrete mathematics and logic, automata theory,
formal methods.
You should be interested in some of the following:
- Obtaining a deeper understanding of programming languages.
- The design and implementation of programming languages.
- Mathematical modelling and the application of discrete mathematics and
logic.
- Computer science research in the area of programming languages.
What Will You Learn?
The main aim of this course will be to introduce the structural,
operational approach to programming language semantics. It will show how
this formalism is used to specify the meaning of some simple programming
language constructs and to reason formally about semantic properties of
programs.
By the end of the course you should be able to:
- be familiar with rule-based presentations of the operational semantics
of some simple imperative, functional and concurrent program constructs;
- be able to prove properties of an operational semantics using various forms of induction;
- be familiar with some operationally-based notions of semantic equivalence of program phrases and their basic properties.
Lecturer
David Sands (dave @cs)
room 5474 in EDIT Building, voice 772 1059 (Chalmers).
Course Literature
You will be able to buy a bound copy of
Pitts' notes at the book shop DC which is located in the ED-building (North
end of the cafe in Linsen.
The price is SEK 60. DC is open 9:45 to 15:15.
(They may run out of copies. You can, of course, print your own copy.)
Additional Reading
-
Hennessy, M. (1990). The Semantics of Programming Languages.
Available here.
- Winskel, G. (1993). The Formal Semantics of Programming
Languages. MIT Press.
- Nielson, H. R and Nielson, F. Semantics with Applications: A Formal Introduction.
Now available online
- VanInwegen and Sewell, How to do Proofs
Overview of the Lectures
- Section 1 and Section 2.1-2.3 in Pitts' notes.
Additional slides.
- Section 2.4 and Section 3.1-3.3 in Pitts' notes.
Also discussed how to model jumps in a machine code language
and in an assembly language. We also discussed what happens if you
try to add gotos to a languge with while statements.
Additional slides.
Additional refs:
- Section 3.4, Section 4 and Section 5.1-5.3 in Pitts' notes.
I also talked about how to model control operators in LC.
Additional slides.
- Section 5.4 and Section 6.1-6.2 in Pitts' notes.
I also talked about how to extend LFP with lists.
Additional slides.
- Section 6.3 in Pitts' notes
(and some new material...)
Additional slides.
LCP is essentially Milner's CCS. See Milner's book for an excellent
introduction
(Milner, R. (1989). Communication and Concurrency. Prentice-Hall.)
In part 2 we looked at the pi calculus.
I handed out Jeannette Wing's FAQ on pi calculus
The following references may also be useful
(taken from http://move.to/mobility):
- Contextual Equivalence: a case study: LC + threads
- A Real-world Case Study (Guest lecture). Koen Claessen will give a gust lecture
about the semantics of PSL, a specification language for hardware. He
will describe its syntax and all the failed attempts by an
international committee to give it a reasonable semantics.
Note that this lecture will be given on Wednesday 16 May, 15-17 (i.e. in the exercise slot).
Exercises/Assignments
The exercise classes for this course are compulsory. If you cannot attend
for some reason then you must hand in your solutions in advance.
At the exercise class we will discuss the weekly
exercises. At the end of the class you will hand in your solutions, and get back solutions from the previous week.
To pass the course you must attend the exercise classes have made a reasonable
attempt at the exercises (as well as the labs and exams).
Exercsises are to be completed individually. May discuss the
problems, but you should write your own solutions.
This year there will be a bonus point system. You may get a bonus point on your exercise solutions if you give particularly interesting solutions to more open ended or optional questions. These bonus points count towards your exam grade.
Exercises
- Exercises for Week 1.
In previous years we discussed a little bit about issues in
providing a semantics for C. Here is a
reference to a PhD on the subject.
- Exercises for Week 2.
- Exercises for Week 3.
- Exercises for Week 4.
- Exercises for Week 5.
- Exercises for Week 6 (corrected 2005).
Course Computer Account
Computer accounts are not used for this course. Please use your own accounts.
You will be expected to find a lab partner, with whom you will do the
assignments (laborations).
The computer assignments ("laborations") are in two parts.
In the first part
you will implement a byte code interpreter and in the second part you
will implement a type based byte code verifier.
There is an optional lab 3, for which you can obtain exam bonus points.
There are no lab supervision times for the labs.
Lab 3 is optional (except for PhD students attending the course).
The lab is to come up with your own extension of the first two
labs. This can either be an extension to the language and type system
(this is the most common extension), or it could be some other kind of
static analysis or program optimisation.
Once you have chosen your extension, you will need to
(i) present the definition of the extension that you propose (e.g. the
operational semantics extension) and (ii) the implementation.
This typically means that for practical reasons you will probably want to extend
the parser - but this should be quite straightforward (the parser is not
written using BNFC but should still be rather easy to extend).
Mail me before the deadline to arrange a time for presentation. This
must be completed before the exam results are reported.
Due date: To be announced. Probably after the exams but before the exam has been graded.
You can receive up to 10 points towards the exam grade for the exam in
May. A maximum of 5 of these points can be used in the case that
you are below the pass-grade for the exam.
You will need a lab partner.
Course Requirement and Examinations
To pass the course, you must have passed the labs, the exercises
and have passed the exam.
The exam (4
hours long) will be held:
2007
INN230/TDA345 Semantics of programming languages
29 May 14.00-18.00
Building V.
V-huset, Sven Hultins gata 6 - see the map of Chalmers campus)
You are permitted to take with you a copy of the lecture notes (i.e.,
Pitts's notes, and the copy of the slides from lecture 6.).
You are not permitted to take other materials (other than a dictionary).
The exam covers material in the lecture notes and the material covered in
lectures 5 and 6.
There is a try out exam which have questions
that are similar in style to the questions that will be on the exam.
This version now contains solutions.
Credits
Lecture notes: A. M. Pitts, Cambridge University.
Exercises and labs developed by J. Gustavsson.
Last modified: Wednesday, 23-May-2007 14:19:28 MET DST
http://www.cs.chalmers.se/Cs/Grundutb/Kurser/nasem/
-Calculus: A Tutorial, (by Robin Milner).
Also available from this site:
[(Postscript)]