| Detailed information |
| Original study plan |
Bachelor's programme Technical Mathematics 2013W |
| Objectives |
Students learn the fundamental approaches to the formal description of the semantics of programmming languages and their relationships; they are able to formalize the semantics of simple languages and implement them in the form of interpreters for these languages.
|
| Subject |
Abstract syntax of programming languages as the basis for the formalization of their semantics.
- Denotational Semantics: the formalization by a mathematical function that maps programs to mathematical structures.
- Operational Semantics: the formalization by a collection of reduction rules that map the initial state of a program to its final state.
- Axiomatic Semantics: the formalization by correctness assertions which allow us to draw conclusions about the input/output behavior of programs.
Proof of the equivalence of denotational and operational semantics of a simple imperative language; proof of soundness of its axiomatic semantics with respect to its denotational semantics; constructive implementation of the denotational semantics in the form of an interpreter.
|
| Criteria for evaluation |
Written homework exercises/mini-projects (formalization of a language with a prototypical implementation as an interpreter).
|
| Methods |
Slide-based lecture with practical examples of formalizations.
|
| Language |
English |
| Study material |
- Wolfgang Schreiner. Thinking Programs (manuscript). Chapter "Programming Languages", 2020.
- David A. Schmidt. Denotational Semantics -- A Methodology for Language Development, Allyn and Bacon, Boston, MA, 1986.
- Glynn Winskel: The Formal Semantics of Programming Languages -- An Introduction, Foundations of Computing Series, MIT Press, Cambridge, MA, 1994.
- David A. Schmidt: The Structure of Typed Programming Languages, Foundations of Computing Series, MIT Press, Cambridge, MA, 1994.
- Hanne Riis Nielson and Flemming Nielson. Semantics with Applications - A Formal Introduction, John Wiley & Sons, 1992.
|
| Changing subject? |
No |
| Further information |
https://risc.jku.at/courses/
|
| Corresponding lecture |
(*)TM1WIVOFSEM: VO Formale Semantik von Programmiersprachen (3 ECTS)
|
