
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.

Subject 
 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)

