Lecture: Semantics
Summer term 2018
News
- June 5
-
The material for the last two lectures on Haskell has been uploaded!
- May 29
-
The material for the first two lectures on Haskell has been uploaded!
- May 25
-
The next four lectures will consist of an introduction to functional programming in Haskell:
- May 28: Basic Haskell
- May 29: Advanced Haskell
- June 4: Monads
- June 5: More monads
The lectures will be given by Sebastian Muskalla.
- March 20
-
The first lecture will take place on April 9.
The first exercise session will take place on April 12.
- March 20
-
The introduction to functional programming in
Organization
-
The lecture will be given by Prof. Dr. Roland Meyer and Dr. Jürgen Koslowski.
-
The dates and room for the lecture are:
-
Monday, 11:30 - 13:00 in IZ 305.
-
Tuesday, 11:30 - 13:00 in IZ 305.
-
The date and room for the exercise classes are:
- Thursday, 9:45 - 11:15 in IZ 305.
Lecture Notes
There are hand-written lecture notes:
There are preliminarey TeX'ed lecture notes on the 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.
If you have questions or spot a bug in the notes, please contact Roland Meyer or Jürgen Koslowski.
Haskell
If you have questions or encounter problems with the exercises, please contact Sebastian.
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.
