02240 - Computability and Semantics

Tentative lecture plan: Please read the material and have a look at the exercises before the lectures.

Abbreviations:

• HMU: Introduction to Automata Theory, Languages, and Computation,
  John E. Hopcroft, Rajeev Motwani, Jefrey D. Ullman, Second Edition, Addison-Wesley, 2001
• NN: Semantics with Applications: An appertizer,
  Hanne Riis Nielson and Flemming Nielson

Every Wednesday the course starts in Building 308, Auditorium 11, at 9.00.

Week (Date)	Topic
5 (2. Feb.)	Lecture 9.00 - 9.45: Course introduction Lecture 10.00 - 10.30: Introduction to the programming exercise: A Pocket Calculator --- to be solved by those knowing SML. Lecture 10.45 - ca. 11.30: Introduction to SML --- intended for those not knowing SML Databar 10.45 - 14.30: For those knowing SML Databar 11.30 - 14.30: Programming exercises --- for those not knowing SML Lecture 14.30 - 15.30: Solution to programming exercises
6 (9. Feb.)	Lecture 9.00 -- 11.00: Natural semantics for a simple WHILE language (NN Ch. 1 and Sec. 2.1). Slides. Exercises 11.00-14.00: 1.2, 1.13, 2.3, 2.4, 2.6, 2.7, 2.10 Lecture 12.30-13.30: For those unfamiliar with SML. Basic types, Lists, Trees, Higher-order functions Lecture 14.00-14.30: Interpreter for natural semantics Databar 14.30-16.30: Programming exercise: implementation of interpreter Lecture 16.30-17.00: Solution to exercises.
7 (16. Feb.)	Lecture 9.00 - 11.00: Structural operational semantics (SOS) for a simple WHILE language (NN Sec. 2.2). Lecture 12.30-13.45: For those unfamiliar with SML. Tautology Checker Exercises 11.00-14.00: 2.16, 2.17, 2.20, 2.21, 2.23, 2.24 Lecture 14.00-14.30: Interpreter for structural operational semantics Databar 14.30-16.30: Programming exercise: implementation of interpreter Lecture 16.30-17.00: Solution to exercises.
8 (23. Feb.)	Lecture 9.00 - 11.00: Comparing two approaches to operational semantics (NN Sec. 2.3 and 3.1) Exercises/Databar 11.00 – 17.00: 2.29, 3.2, 3.5, 2.11 and 3.6.
Deadline: 1^st March	Compulsory exercise: “Everything one would like to know about the repeat construct – and a little bit more” to be handed in on March 1^st (please use the mailbox on the ground floor of building 322, west end). Exercises: 2.7, 2.10, 2.17, 2.24 and 2.29 Programming exercises: implementations of NS as well as SOS for the while language extended with the repeat construct (including well-chosen test programs illustrating how the implementations work).
9 (2. March)	Lecture 9.00 - 11.00: Procedures (NN Sec. 3.2) and pointers (notes) Exercises: 3.9, 3.10, 3.11, 3.13, 3.17 Lecture 14.00-15.00: Reference monitor semantics for security (slides) Databar: extension of NS to a reference monitor semantics (see page 10 of the slides)
10 (9. March)	Lecture 9.00 - 11.00: Provably correct implementation (NN chapter 4) Exercises: 4.7, 4.16, 4.8, 4.17, 4.23, Questions 4 and 5 from here. Lecture 14.00-15.00: More on probably correct implementation Exercises
11 (16. March)	Lecture 9.00 - 11.00: Non-interference (draft available here) Exercises: see draft Lecture 13.00-15.00: Solutions to compulsory exercise 1 Databar: 15.00-17.00
Deadline: 31st March	Compulsory exercise to be handed in on March 31st (please use the mailbox on the ground floor of building 322, west end). Exercises: 4.7 and 4.16 from [NN] and exercises 2 and 5 of draft. Programming exercises: reference monitor semantics (see slide 10 of slides) together with one (!) of the following programming exercises: non-interference algorithm (Exercise 3 of draft), or code generation and implementation of abstract machine as specified in exercises 4.7 and 4.16. In both cases this includes well-chosen test programs illustrating how the implementations work.
13 - 18 (30. March - 4. May)	The topic is computability. Course material is in the book HMU Chapters 8 and 9. In this part, there will be two mandatory assignments. The full text of the first of them is found here and the associated program here. Assignment 3 should be handed in on April 20. Parts of this assignments are solved in the databar in on March 30. and April 6. (See below.)
13 (30. March)	Lecture 9.00 - 12.00: Introduction to Computability, Turing Machines. HMU 8.1 and 8.2. Databar 13.00 - 17.00: Exercises HMU 8.2.1(b,c), 8.2.2(b,c) Exercise using Turing Machine Simulator and associated program TM1.sml. Test your solution to 8.2.2(b,c) on the simulator.
14 (6. April)	Turing Machine Programming Techniques HMU 8.3-7. Exercise class 13.00 -15.00: Exercises HMU 8.4.1(8.2.2(b,c)), 8.4.2(a), 8.5.1(b,c), 8.3.2 Databar 15.00 - 17.00: Part II, exercises (c,d,e) of the assignment 3 (associated program)
15 (13. April)	Universal Turing Machine, Undecidability HMU 9.1-3. Exercise class 13.00 -14.30: Exercises HMU 9.1.3(a), 9.2.6(b,c), 9.3.6(a), 9.3.7(b) Databar 14.30 - 17.00: Work on assignment 3.
16 (20. April)	Lecture 9.00 - about 11.30: Undecidability HMU 9.4-5. Short introduction to tiling problems. See, for example, Wang tiles (or Wang dominoes or aperiodic tiling Dedicable and undecidable problems for Duration Calculus, a real-time interval logic. Mandatory assignment 4 is handed out. Databar 13.00 - 17.00: Work on assignment 3 and assignment 4. Deadline of assignment is 17.00.
17 (27. April)	No lecture. Work on the 4. mandatory assignment. Exercise class 10.00 - 12.00: The teaching assistant (Aske Brekling) answers questions concerning the 4. mandatory assignment.
18 (4. May)	Course evaluation. Deadline of 4. mandatory assignment.