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: 8 Units of 5 hours each: 40 Std
Exercises: 50 Std
Exam (including preparation time): 22 Std
Start: The course starts on 5.3.2018.
Lecture/exercise/examen dates
5.3. intro/ lecture FO part1
7.3. lecture FO part2 /ex-FO online
12.3. lecture1
14.3. lecture2/hand-in ex-FO/ex1 online
19.3. exercise FO
21.3. repitition
26.3. Easter holidays
28.3. Easter holidays
2.4. Easter holidays
4.4. Easter holidays
9.4. lecture3/hand-in ex1/ex2 online
11.4. lecture4
16.4. exercise1
18.4. lecture5/hand-in ex2/ex3 online
23.4. lecture6
25.4. exercise2
30.4. lecture7/hand-in ex3/ex4 online
2.5. lecture8
7.5. exercise3
9.5. no lecture
14.5. no lecture
16.5. lecture9/hand-in ex4/ex5 online
21.5. Pfingstmontag / public holiday
23.5. exercise4/hand-in ex5
28.5. TBA
30.5. exercise5
4.6. TBA
6.6. exam1
11.6. no lecture
13.6. no lecture
18.6. no lecture
20.6. no lecture
25.6. exam2
27.6. no lecture
------
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:
The first two lectures will repeat first-order logic and can be skipped by students who have mastered the material. This year 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 8 lectures and 5 exercises. After every two lectures there is one exercise. Students have to solve the initial exercise sheet on first-order logic and plus the 5 exercise sheets and get at least 40% of the total points in order to be admitted to 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.
