185.205 Semantik von Programmiersprachen / Semantics of Programming Languages, VU 3.0/2.0

Lecturer: Bernhard Gramlich.

Language: The course is (usually) held in English.

This course is primarily intended for students in computer science and mathematics, who are interested in formal and theoretical foundations of programming languages. It is an optional or mandatory course, respectively, in the new Master Studies Computational Intelligence, Software Engineering & Internet Computing, Technische Informatik and in Computational Logic (European Masters Program in Computational Logic).

News

• ATTENTION: In order to avoid an overlap with the course Komplexitätstheorie (181.142), the dates have been slightly changed (now: half an hour earlier: Tuesday, 8:45-10:15, see below!)

• Registration for the course via TUWIS++ is possible here.

• Dates:
  • First class: Tuesday, 09.03.10, 9:15-10:45, EI 1 Petritsch HS
  • Regular date: Tuesday, 8:45-10:15, EI 1 Petritsch HS

• Combination/Deepening: In parallel to this course there will also be a Seminar in Theoretical Computer Science with thematic focus "Semantics of Programming Languages" in the summer term 2010. Participation in the seminar is recommended, too (but no precondition for attending the course)!

Contents

The course deals with basic foundations of (formal) semantics of programming languages. For a real understanding of programs in any programming language and especially for logical reasoning about properties of such programs a clearly defined semantics is indispensable. There exist various different approaches to describe the formal semantics of programming languages. In the course we treat, among other approaches, operational, denotational, and axiomatic (definitions of) semantics, as well as the relationships between these different formalisms.

Prerequisites

Basic knowledge in the fields (courses) Einführung in die Theorie der Informatik / Theoretische Informatik 1 / Theoretische Informatik und Logik / (alternatively here) and Theoretische Informatik 2 / Formale der Methoden Informatik (OLD) / Formale der Methoden Informatik (NEW) is assumed.

Literature

The course primarily relies on the following textbook(s):

• Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: Formal Introduction, Wiley Professional Computing, 240 Seiten, ISBN 0 471 92980 8, Wiley, 1992.
• Hanne Riis Nielson and Flemming Nielson: Semantics with Applications: A Formal Introduction, revised edition, 1999 (see also here).
• Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: An Appetizer. Springer Series: Undergraduate Topics in Computer Science, 274 p. 4 illus., Softcover, ISBN: 978-1-84628-691-9, 2007.

• Daniel P. Friedman, Mitchell Wand, and Christopher T. Haynes: Essentials of Programming Languages, MIT Press (trade, ISBN 0-262-06145-7) and McGraw Hill (academic, ISBN 0-07-022443-9), 536 Seiten, 1992.
• Glynn Winskel: The Formal Semantics of Programming Languages - An Introduction, MIT Press, Cambridge Massachusetts, 361 Seiten, ISBN 0-262-23169-7, 1993.
• John C. Mitchell: Foundations for Programming Languages, MIT Press, Cambridge, Massachusetts, 846 Seiten, ISBN 0-262-13321-0, 1996.
• Joseph A. Goguen, Grant Malcolm: Algebraic Semantics of Imperative Programs, MIT Press (Series: Foundations of Computing), 228 Seiten, ISBN 0-262-07172-X, 1996.
• Carl A. Gunter: Semantics of Programming Languages, MIT Press, 419 Seiten, ISBN 0-262-07143-6, 1992.
• Matthew Hennessy: The Semantics of Programming Languages: An Elementary Introduction using Structural Operational Semantics, Wiley 1990.
• John C. Reynolds: Theories of Programming Languages, Cambridge University Press, 500 Seiten, ISBN 0-521-59414-6, 1998.

Copies of the slides used in the course will be available.

Assessment

Assessment will be based on an exercises part and a written final exam towards the end of the course. In order to successfully pass the course, positive results in both the exercises part and the final exam are necessary.

In particular, the exercises part includes a first (written) test (after the Easter break) which covers basic theoretical/mathematical/logical foundations that are assumed in the course (as e.g. taught in Theoretische Informatik und Logik, cf. also here, and Formale Methoden der Informatik), as well as material treated so far in the first classes of the course. Detailed information about this first (obligatory) test, the final exam and the overall assessment will be given in the course (on Tuesday, March 16, 2010).

Exams

• Exercises exam: 13.04.10, 08:45-10:15, INF-HS (registration via TUWIS++ necessary, 12.03.-11.04.10)
  What you should know for this exercises exam:
  • General prerequisites:
    • basics in theoretical computer science and logic, and in formal methods
    • how to argue, reason and prove results in a formally (mathematically/logically) correct way
    • basic proof principles (by induction, by contradiction, ...)
    • basic knowledge about programming languages
  • Course material covered so far, in particular:
    • natural and structural operational semantics
    • definitions, proof principles, proofs of simple properties
    • important notions like semantic equivalence, determinism, (non-)termination of programs and their application on examples
  Only allowed during the exercises exam: Copies of slides and own lecture notes (from the course), no (copies of) books!

• Final exam: 29.06.10, 08:30-10:30, INF-HS (registration via TUWIS++ necessary, 01.06.-27.06.10)
  Only allowed during the final exam: Copies of slides and own lecture notes (from the course), no (copies of) books!

Bernhard Gramlich | AB Theoretische Informatik und Logik | Fakultät für Informatik | TU Wien