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
Contents:
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
Literature:
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.
Software:
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.
Slides:
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
Webmaster