Lecture: Semantics
Winter term 2019/20
News
- October 2
-
The first lecture will take place on Tuesday, October 29 in IZ 358.
Organization
-
The lecture will be given by Prof. Dr. Roland Meyer and Sören van der Wall.
-
Entry in the list of lectures:
Lecture,
Exercises.
-
The dates and room for the lecture are:
-
Tuesday, 11:30 - 13:00 in IZ 358.
-
Wednesday, 11:30 - 13:00 in IZ 358.
-
The date and room for the exercise classes are:
- Thursday, 11:30 - 13:00 in IZ 358.
Exercise Sheets
Lecture Notes
There are few slides and hand-written lecture notes:
There are preliminarey TeX'ed lecture notes on some categorical
aspects: identifying the monad underlying alternating automata, and
connections between the simply typed Lambda-calculus and (cartesian)
closed categories. In addition, notes on two different approaches to
monads have been added.
Further literature recommendation: chapter 1 of the book "Homotopy
Type Theory" provides a nice introduction into (internal) Martin-Löf type
theory, which extends the Lambda-Calculus with dependent types. It
points out the crucial differences between set theory and type theory and aims to
prepare for the new approach involving homotopy theory (presently beyond our
scope). A PDF-version
is freely available.
Module
Successfully finishing the module consists of two parts:
- Prüfungsleistung: Oral exam after the lecture period.
- Studienleistung: Get at least 60% of all points on your submitted solutions of the exercise sheets.
Contents
-
Functional programming
- Functional programming in Haskell
- Higher-order functions
- Monads
- Lambda calculus
- Normal forms
-
Types
- Hindley-Milner type inferenz
- Dependent types
- Refinement types
- Liquid types
- Resource consumption as an application
-
Higher-order model checking
- Higher-order recursion schemes
- Monadic second-order logic and the model-checking problem
- Type-based approach
- Game semantics
- Game-semantics-based algorithm
- Game semantics and full abstraction
-
Effective denotational semantics
- Models and fixed points
- Walukiewicz and Salvati's result
- Models for infinite computations
- Models for alternation
- Fixpointtransfer
- Outlook on k-CFA
-
Domains
- Categories and closure properties
- Recursive systems of equations
- Kleene, Békic and Newton
- Powerdomains
- Sheaves
-
Linear logic
- Linear logic
- Curry-Howard isomorphism
-
Alternative models
- Caucal's hierarchy
- Logical interpretation
- Coincidence with higher-order schemes
- (Collapsible) higher-order pushdown automata
- Coincidence with higher-order schemes
- Saturation
Literature
The lectures will be based upon the following books and articles. Most of them are available online.
-
Naoki Kobayashi, C.-H. Luke Ong:
A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. LICS 2009: 179-188.
-
C.-H. Luke Ong:
On Model-Checking Trees Generated by Higher-Order Recursion Schemes. LICS 2006: 81-90.
-
B. Khoussainov, A. Nerode. Automata Theory and its Applications. Birkhäuser, 2001.
-
M. Hofmann and M. Lange. Automatentheorie und Logik. Springer-Verlag, 2011.
-
Th. Cachat. Symbolic Strategy Synthesis for Games on Pushdown Graphs. In Proc. of the 29th International Colloquium on Automata, Languages and Programming, ICALP, pages 704-715, Springer, 2002.
-
I. Walukiewicz. Pushdown Processes: Games and Model Checking. In Journal Information and Computation - Special issue on FLOC '96, pages 234-263. Academic Press, 2001. Pages 234-263
-
L. Holik, R. Meyer, S. Muskalla. Summaries for Context-Free Games. In Proc.of 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, pages 41:1-41:16. LIPIcs, 2016.
-
O. Serre. Note on winning positions on pushdown games with omega-regular winning conditions. In Information Processing Letters, Vol 85 Issue 6, pages 285-291. Elsevier, 2003.
-
D. A. Martin. A purely inductive proof of Borel determinacy. In Proc. Sympos. Pure Math., Vol 42, page 303-30. AMS, 1985.
-
U. Zwick, M. Paterson. The complexity of mean payoff games on graphs. In Theoretical Computer Science, Vol. 158, Issues 1-2, pages 343-359. Elsevier, 1996.
