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
- limits of provability: Goedel's Incompleteness Theorems (Stanford Encyclopedia).
- from Turing Machines to lambda-calculus and back: relating models of computation
- from formulas to types: the Curry-Howard Correspondence
-
intuitionistic logic and program extraction; correctness by generation
example tool: Coq -
from word/string automata to tree automata
(Tata)
example tool: Timbuk -
from SAT to Satisfiability Modulo Theories
(DPLL(T))
example tool: Yices -
from induction to coinduction; bisimulation in concurrency
(Davide Sangiorgi)
-
LTL (linear temporal logic) model checking
example tool: Spin -
process calculi for concurrency
example tool: mCRL2 -
interactive theorem proving
(history)
example tool: Isabelle/HOL -
automated theorem proving and the superposition calculus
example tool: eprover -
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.