Semantic Methods (Semantiska metoder)

Course texts

• [MTD] Viggo Stoltenberg-Hansen, Ingrid Lindström, Ed Griffor, Mathematical Theory of Domains, Cambridge University Press 1993.
• [DTF] Thomas Streicher, Domain-Theoretic Foundations of Functional Programming, World Scientific Publishing 2006. Earlier version (2004) available in prepublication form (compressed PDF).
• Articles and papers (available electronically from the library)
  • [E] M.H. Escardo. PCF extended with real numbers. Theoretical Computer Science 162 (1996), 79 - 115.
  • [EE] A. Edalat and M.H. Escardo. Integration in Real PCF. Information and Computation 160 (2000), 128 - 166.

Other texts

• Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction. MIT Press 1993

Lectures

1. Fr 22/1. Fixed points. Continuous functionals on partial functions. Kleene's recursion theorem. (Ch 1.1 in MTD)
2. Mo 25/1. Omega-cpos, cpos. (Ch 0.2, 1.2, 2.1 in MTD)
3. We 27/1. Cartesian products and function spaces in Cpos. Cartesian closed categories. (Ch 0.3, 2.2, 2.4 in MTD)
4. Fr 29/1. Cartesian closed categories (cont.) PCF and its operational semantics. (Ch 2 in DTF)
5. Mo 1/2. Operational semantics (Cont.) Scott's model of PCF. (Ch 3 in DTF)
6. Tu 2/2. Scott's model (cont.). LCF.
7. Fr 5/2. Computational adequacy of Scott's model. Logical relations. The full abstraction problem. (Ch 4-5 in DTF)
8. Mo 8/2. Compact elements. Algebraic domains. Scott domains. Presentations of domains by cusls. (Ch 3 in MTD)
9. We 10/2. Problem session. Exercises 1 (PDF).
10. We 17/3. Presentations of domains: generating infinite terms from finite terms. Compact elements in function spaces.
11. Fr 19/3. Basic notions of topology. Alexandrov topology and Scott topology. (Ch 5 in MTD)
12. Mo 22/3. Review of recursion theory. Computability in domains.
13. We 24/3. Computability and domains. Full abstraction and universality for extensions of PCF.
14. Mo 12/4. Universality for extended PCF. Total continuous functionals.
15. Mo 19/4. Real numbers and domains. Real PCF. (See [E] and [EE])
16. We 21/4. Functors. Algebras and coalgebras relative to an endofunctor. Inductive, coinductive and recursive types
17. Fr 23/4. Domain equations: direct limits in general categories and in Cusl
18. Mo 26/4. Domain equations in Cusl. Natural transformations and equivalences of categories.
19. On 28/4. Domans equations in Dom. Models of untyped lambda calculus.
20. Mo 3/5. Guest lecture, or rather the Mathematics Colloquium, room Å2001, 15.15-16.15.
21. Mo 10/5. Monads.
22. On 12/5. Semantics for imperative languages.
23. Mo 17/5. Operational interpretations of linear logic. Linear lambda calculus.
24. Fr 28/5. Categorical semantics of linear logic.
25. Supervision of Assignment 5. Make an appointment with me.

Schedule and Syllabus

• Schedule
• Syllabus of the course in English and in Swedish.

Examination and Assignments

• Assignments 1 - due March 19.
• Assignments 2 - due March 24.
• Assignments 3 - due April 21.
• Assignments 4 - due May 24.
• Assignment 5: write a short report on a paper or book chapter.