Semantics of Programming Languages

Lecture in summer semester 2014

Instructor: Dr. Mihai Codescu
Language: English
Weekly timeplan: 2 + 2 + 0
Intended audience: Bachelor Informatik Semester 5 and 6, Master Computervisualistik, Master DKE, Master Informatik

Schedule change: the Tuesday meeting has been moved to Wed 13-15, room G22A-210


Operational semantics for IMP: definition of big-step semantics, definition of small-step semantics, their equivalence
Denotational semantics for IMP: definition, equivalence with operational semantics
Axiomatic semantics for IMP: definition, soundness of Hoare calculus
Introduction to K semantic framework
Semantics of IMP and other programming languages in K
Type systems


G. Winskel - The Formal Semantics of Programming Languages - An Introduction, MIT Press 1994
T. Nipkow, G. Klein - Concrete Semantics, A Proof Assistant Approach, 2014
T. Serbanuta et al - The K Primer
G. Rosu, T. Serbanuta - K overview and SIMPLE case study

Resources for the lecture are here.


See the installation instructions for the K tool at the home page of K. Use the latest stable release, and notice that in path/to/K/lib/scripts/ you have to do "chmod a+x checkJava" to be able to run the K tools.


Lecture 1: General overview, I/O language for "Hello World!", "Hello world!" program.
Lecture 2: Operational semantics
Exercise 1: Operational semantics
Lecture 3: Denotational semantics
Exercise 2: Denotational semantics
Lectures 4-5: K quick reference, IMP syntax, sum program in IMP Non-determinism, non-deterministic print.
Lectures 6-7: Adding new features to IMP
Lectures 8-9: IMP++ in K, archive with files
Lectures 10: Project ideas
Lectures 11: Functions in IMP
Lectures 12: Axiomatic semantics for IMP
Lectures 13: Matching logic

Exercise sheets:
Exercise sheet 1 23.04, due 30.04

Zur Lehreseite der Forschungsgruppe Theoretische Informatik