Inhalt

[ 201LOSDFPLV13 ] VL Formal Semantics of Programming Languages

Versionsauswahl
(*) 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 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)
On-site course
Maximum number of participants -
Assignment procedure Direct assignment