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 start at 3.3.2014.

Lecture/exercise/examen dates

3.3. lecture FO part1

7.3. lecture FO part2/ex-FO online

10.3. lecture1

14.3. lecture2/hand-in ex-FO/ex1 online

17.3. exercise FO

4.4. repitition

7.4. lecture3/hand-in ex1/ex2 online

11.4. lecture4

14.4. exercise1

18.4. lecture5/hand-in ex2/ex3 online

21.4. lecture6

25.4. exercise2

28.4. TBA(probably no lecture)

2.5. lecture7/hand-in ex3/ex4 online

9.5. lecture8

12.5. exercise3

19.5. TBA(probably no lecture)

23.5. TBA(probably no lecture)

30.5. last lecture/hand-in ex4/ex5 online

2.6. TBA(probably no lecture)

6.6. exercise4/hand-in ex5

9.6. TBA(probably no lecture)

13.6. exercise5

16.6. TBA(probably no lecture)

20.6. exam1

23.6. no lecture

27.6. no lecture

30.6. exam2

 ------

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.

Participation in this course requires passing an entrance exam, which will take place during the third lecture. The entrance exam will be about first-order logic and performing simple proofs in a rigorious way (see lecture requirements). The entrance exam will be graded according to the precision of mathematical formulation and reasoning. The entrance exam can either be passed or not passed and will not contribute to the final grade.

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.

These requirements will be tested in the entrance exam.