Acquisition of basic knowledge (foundational formalisms and definition methods) for the semantic description and characterization of programming languages and programming constructs. Learning of methodological criteria for the analysis and the proof of correctness of a program with regard to the semantics of the respective programming language.
Foundational semantic description methods and formalisms: Operational, denotational and axiomatic semantics of imperative program constructs; relations to program verification; introduction to the lambda-calculus; inductive and recursive definitions; fixed point operators and constructions; selected topics like non-determinsim and concurrency.
ECTS Breakdown: ECTS 4.5 = 112h
Lectures: 5 Units of 8 hours each: 40 Std
Exercises: 50 Std
Exam (including preparation time): 22 Std
Start: The course start at 8.6.2017.
Lecture/exercise/examen dates
8.6. lecture FO-part1/lecture FO-part2/exercise-FO online
9.6. lecture1/lecture2
12.6. exercise-FO/exercise-sample/exercise1 online
13.6. lecture3/lecture4
14.6. exercise1
16.6. lecture5/lecture6
19.6. exercise2
20.6. lecture7/lecture8
21.6. exercise3
22.6. TBA (probably no lecture)
23.6. exercise4
26.6. TBA (probably no lecture)
27.6. exercise5
30.6. Written Exam
There will be a second exam in the first week of WT17/18, the exact date is to be announced.
------
Further Reading:
"Introduction to lattices and order", B. A. Davey and H. A. Priestley is a good introduction to lattice theory
"Types and Programming Languages", Benjamin Pierce is the standard introduction into types in programming languages
Structure of the course:
This year the lecture is taking place blocked in June.
(In 2018 the lecture is going to be spread evenly over the sommer term again.)
The first lecture will repeat first-order logic and can be skipped by students who have mastered the material. There will be no entrance exam. However, the first exercise sheet assumes familiarity with first-order logic and basic set-theoretic and logical notations.
The main part of the lecture concists of 4 lectures and 6 exercises.
In each exercise session we will discuss one exercise sheet. The exercise sheet is put online in time, such that the students can engage with the exercise questions and prepare for the exercise session. There is no requirement to submit a solution to the exercise questions. The written exam will be closely related to the exercise questions. Thus, an intensive interaction with the exercise material is essential for a successful participation in the exam.
Basic knowledge of first-order logic (FOL) as introduced in the courses 185.278 and 185.291; in particular, understanding the difference between syntax and semantics and being able to use structural induction for proving properties of FOL formulae.
Basic knowledge of Hoare-logic as introduced in185.291.
Working knowledge of set-theoretic and logical notation; in particular, being able to precisely formulate and prove mathematical statements as taught and practiced in the coureses 104.271, 185.278, 185.291.
