Description

Computational Logic is concerned with the logical foundations of computer science and their application to the analysis and verification of complex systems. This is largely reflected in the various courses taught by CL, e.g. Introduction to Theoretical Computer Science, Functional Programming, Logic, Logic Programming, and Term Rewriting in the Bachelor Program, and Computability Theory, Automated Theorem Proving, Interactive Theorem Proving, Formal Language and Automata Theory, Computational Logic.

In this Specialisation Seminar we will look at selected topics from Computational Logic going beyond those taught in the Bachelor Program, and (mostly) giving an outlook on those taught in the Master Program. In order to treat each selected topic in sufficient depth, it needs to be taken by (exactly) two students.

Topics

1. limits of provability: Goedel's Incompleteness Theorems (Stanford Encyclopedia).
2. from Turing Machines to lambda-calculus and back: relating models of computation
3. from formulas to types: the Curry-Howard Correspondence
4. intuitionistic logic and program extraction; correctness by generation
   example tool: Coq
5. from word/string automata to tree automata (Tata)
   example tool: Timbuk
6. from SAT to Satisfiability Modulo Theories (DPLL(T))
   example tool: Yices
7. from induction to coinduction; bisimulation in concurrency (Davide Sangiorgi)
   
8. LTL (linear temporal logic) model checking
   example tool: Spin
9. process calculi for concurrency
   example tool: mCRL2
10. interactive theorem proving (history)
    example tool: Isabelle/HOL
11. automated theorem proving and the superposition calculus
    example tool: eprover
12. from first-order to higher-order unification
    example tools: lambdaProlog, Isabelle.

We will look at (at most) 9 topics among the ones listed above. A topic needs to be taken by two students, who will give a joint presentation and who will write a joint report.

Guidelines

The final grade will be based on the presentation (40%) and the written report (40%) . Active participation during the presentations will also be taken into account (20%). In particular, attendance each week (when there is a seminar, see the overview) is mandatory.

Language and Typesetting

Theses must be written in LaTeX2e. In order to ensure a uniform layout, the Computational Logic LaTeX class must be used. Before producing the final version of the seminar report, make sure you use the latest version. Reports have to be written in English. The report must be between 10 and 15 pages long.