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 4.3.2019.
Lecture/exercise/examen dates for the summer term 2019
4.3. intro/ lecture FO part1
6.3. lecture FO part2 /ex-FO online
11.3. lecture1
13.3. lecture2/hand-in ex-FO/ex1 online
18.3. exercise FO
20.3. repetition
25.3. lecture3/hand-in ex1/ex2 online
27.3. lecture4
1.4. exercise1
3.4. lecture5/hand-in ex2/ex3 online
8.4. no lecture
10.4. exercise2
15.4. Easter holidays
17.4. Easter holidays
22.4. Easter holidays
24.4. Easter holidays
29.4. TBA
1.5. public holiday
6.5 lecture6
8.5. lecture7/hand-in ex3/ex4 online
13.5. lecture8
15.5. exercise3
20.5. lecture9/hand-in ex4/ex5 online
22.5. TBA
27.5. exercise4/hand-in ex5
29.5. TBA
3.6. exercise5
5.6. TBA
10.6. Holiday
12.6. exam
17.6. no lecture
19.6. no lecture
24.6. no lecture
26.6. if needed: exam repetition
------
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.
