Semantik

Inhalt

Formale Semantiken von Programmiersprachen liefern ein mathematisches Modell der Programmausführung. Sie bilden die Grundlage für den Nachweis von Eigenschaften sowohl der Programmiersprache, zum Beispiel Typsicherheit, als auch von Programmen, beispielsweise mittels Verifikation. Darüber hinaus spielen Semantiken bei der Implementierung von Programmiersprachen eine wichtige Rolle: Interpreter können zum Beispiel automatisch aus einer formalen Semantik generiert werden.
Daher gehört die Beschreibung und Nutzung formaler Semantiken zum Handwerkszeug von Informatikern, die sich fundiert mit Programmierung und Programmiersprachen befassen.
Diese Vorlesung gibt eine grundlegende Einführung in die Semantik von Programmiersprachen. Sie erläutert die operationelle, denotationale und axiomatische Semantik eine Sprache sowie deren Beziehungen untereinander. Darüber hinaus werden typische Anwendungen dieser Semantiken besprochen und an Beispielen illustriert.

Ziel

Ziel der Vorlesung ist es, die grundlegenden Techniken zur präzisen Definition der Semantik einer Programmiersprache zu verstehen und diese Techniken anzuwenden auf Probleme wie die Äquivalenz verschiedener Sprachbeschreibungen, Programmkorrektheit oder die Korrektheit von Programmtransformationen.

Dozent

Müller, P.

Umfang/Credits

2V1U (5 Credits)

Sprache

Vorlesung: Deutsch
Übung: Englisch

Voraussetzungen

Programmiererfahrung

Literatur

Hanne Riis Nielson, Flemming Nielson: Semantics with Applictions: A Formal Introduction. Wiley, 1992.
http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html

Betrand Meyer: Introduction to the Theory of Programming Lanuages. Prentice Hall, 1990

Glynn Winskel: The Formal Semantics of Programming Languages. The MIT Press, 1993.

Carl A. Gunter: Semantics of Programming Languages. The MIT Press, 1992

John C. Mitchell: Foundations of Programming Languages. The MIT Press, 1996

Krzysztof R. Apt, Ernst-Rsudiger Olderog: Verification of Sequential and Concurrent Programs. Springer-Verlag, 2nd ed., 1997

David Harel, Dexter Kozen, Jerzy Tiuryn: Dynamic Logic. The MIT Press, 2000

Dorothy E.Denning: A Lattice Model of Secure Information Flow. Purdue University

Andrei Sabelfeld and Andrew C.Myers: Language- Based Information-Flow Security. IEEE Journal on Selected Areas in Communications, VOL. 21, NO.1, January 2003

Dennis Volpano, Geoffrey Smith, Cynthia Irvine:A Sound Type System for Secure Flow Analysis. Journal of Computer Security, draft printout, 29 Jul 1996,1-20 IOS Press

A. Poetzsch-Heffter and P. Müller: A Programming Logic for Sequential Java.
In Programming Languages and Systems, Pages 162-176, Springer-Verlag, 1999.

A. Poetzsch-Heffter and P. Müller: Logical Foundations for Typed Object-Oriented Languages.
In Programming Concepts and Methods, 1998.