[ 201LOSDFPLV13 ] VL Formal Semantics of Programming Languages

(*) Unfortunately this information is not available in english.
Workload Education level Study areas Responsible person Hours per week Coordinating university
3 ECTS B3 - Bachelor's programme 3. year Mathematics Wolfgang Schreiner 2 hpw Johannes Kepler University Linz
Detailed information
Original study plan Bachelor's programme Technical Mathematics 2013W
Objectives Students shall learn the fundamental approaches to the formal description of the semantics of programmming languages and their relationships; they shall become themselves able to formalize the semantics of simple languages.
  • 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.

Criteria for evaluation Written homework exercises.
Methods Lecture with practical examples of formalizations.
Language English
Study material
  • 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
Corresponding lecture (*)TM1WIVOFSEM: VO Formale Semantik von Programmiersprachen (3 ECTS)
On-site course
Maximum number of participants -
Assignment procedure Direct assignment