Master Theme Foundations of Computer Science

Coordinator: Prof.dr. J.H. Geuvers.

In the Foundations group, we study the mathematical oriented models of computing and reasoning. The keywords are: Computability, Provability and Complexity. More specifically we perform research in the following topics: Type Theory, Lambda calculus, Theorem Proving, Complexity Theory and Computer mathematics. Foundations is one of the possible themes in a Computer Science master programme at the Radboud University Nijmegen. The teaching will be done by staff from the Foundations (F) group.

The Foundations theme deals with abstract mathematical models of computing and reasoning. These are studied both for their own (theoretical) interest as for their applicability in other research areas. Computing and reasoing meet in the area of "Formalized Mathematics". The foundations group contributes to the challenging development of "Computer Mathematics", a unified system for (symbolic) computing and reasoning. The courses "Type Theory" and "Proof Assistants" are part of that thread. Students with a specific interest in Computer Mathematics are strongly encouraged to also follow courses in Computer Algebra in the Mathematics Department. We also study the basis of formal methods and more in general, formalisms to analyze computer systems and programs. Formal Methods is nowadays applied in various areas of Computer Science, so this is also a challenging field. The courses "Semantics", "Complexity" and "Type theory" are part of this thread. Students with a specific interest in the mathematical basis of Formal Methods are strongly encouraged to also follow logic-related courses in the Mathematics Department. The themes we study are pervasive in Academic Computer Science. We have a lot of contacts with other research groups (in the Ntherlands, Europe, the US and Japan) and regular visitors from outside. Students are strongly encouraged to participate in this (in)ternational research network.

The Foundations master theme involves the next four compulsory courses (1-4) within the NIII, each amounting to 6 EC. For each course, the number of students is limited, so get in touch with the teacher to find out when and how the course is actually given

  1. Type Theory (Wiedijk, spring semester).
    This course covers dependent type theories, with an emphasis on the use of these systems for formalizing mathematics and theorem proving. It partly builds on top of Semantics and Correctness, T3, where the lambda calculus is introduced.
  2. Complexity (van Leijenhorst, spring semester).
    This course builds on the introductory complexity course Analysis of Algorithms, T2.
  3. Proof Assistants (Wiedijk, spring semester).
    This course introduces various systems for formalizing mathematics: Coq, HOL, PVS and Mizar. Both implementation techniques and the formal logical backgrounds will be discussed. The course is based on a forthcoming book by John Harrison on this subject.
  4. Semantics (Geuvers, fall semester).
    This course covers semantics of functional and imperative languages and operational and denotational semantics of the untyped lambda calculus. It builds on top of Semantics and Correctness, T3, or if you are a more recent student, on Semantics and Logic 1 and Semantics and Logic 2.

Within Computer Science the following supplemental courses are recommended.

Students are encouraged to follow additional courses in mathematics There is currently no ready-to-use set of courses in mathematics available, so interested students are advised to find suitable courses themselves and discuss these with the theme's coordinator.

Outside Nijmegen, students may be interestes to follow relevant courses for instance in Eindhoven (within computer science or mathematics) or at the Free University of Amsterdam. Some suggestions:

Part of a master program is a master thesis. Members of the Foundations group and teachers within this theme may serve as supervisors for such a master thesis. They may be contacted directly to discuss various options and ideas.