Formal Semantics of Programming Languages (SS 2023)
Abschnittsübersicht
-
326.0FS, Time: Friday, 8:30-10:00, HS 13, Start: March 10, 2023.While the syntax of a programming language is always formally specified, the equally important aspect of definining its meaning is often left to natural language which is ambiguous and leaves many questions open. In order to understand the inherent properties of a language (e.g. for constructing a compiler), we should have a deeper understanding. This course presents some major methods for defining the formal semantics of programming languages (and thus programs) and discusses their relationship:
- Denotational Semantics
- A programming language is defined by a valuation function that maps a program into a mathematical object which is considered as its meaning.
- Operational Semantics
- A programming language is defined by reduction rules that describe how the initial state of a program is transformed step by step into the terminal state.
- Axiomatic Semantics
- A programming language is defined by correctness assertions that describe how to draw conclusions about the input/output interface of a program.
The participants are expected to elaborate a small project (the implementation of some semantics presented in class) which will be used for grading (there will be no final exam).
To participate in the course, you have to register in the KUSSS System. Since the assignments will be uploaded in Moodle, you also have to create an account in the RISC Moodle (press the button "Create new account", you have to register with your jku.at email address) and self-enrol in the course (press the button "Enrol me"); then you also receive all messages posted in the course forums per email.
-
As an extra service, it is intended to live-stream and record the lectures via the following Zoom meeting:
https://jku.zoom.us/j/93033164127?pwd=N0w3T2QzZENxcEQzY21IQisrbkdEZz09
Meeting-ID: 930 3316 4127 Password: formalsemHowever, no guarantee is given with respect to completeness and quality of the stream/recordings. The basic course format is on-site, not hybrid.
-
The lecture will be based on Chapter 1 "Syntax and Semantics" and Chapter 7 "Programming Languages" of the book "Thinking Programs"; in the course we will walk through most parts of these chapters (the book can be freely downloaded in the JKU campus network).
Variously we may also use material from previous instances of this course (not aligned with above chapters):- Denotational Semantics (Part 1)
- Denotational Semantics -- A Methodology for Language Development: Chapters 1-5.1
- Operational Semantics
-
Introduction to Operational Semantics (restricted)
-
IMP: a Simple Imperative Language (restricted)
-
Big Step Structural Operational Semantics (restricted)
-
Small Step Structural Operational Semantics (restricted)
-
Modular Structural Operational Semantics (restricted)
-
Equivalence to Denotational Semantics (restricted)
- Denotational Semantics (Part 2)
- Denotational Semantics -- A Methodology for Language Development: Chapters 6 and 5.2--5.4
- Languages with Contexts
- Axiomatic Semantics
- The Axiomatic Semantics of IMP (restricted)
-
Grading will be based on a small project (the implementation of the semantics presented in class) consisting of two mandatory and an optional assignment.
-
