Up: Cooperating sites
Previous: Udine


The Applied Logic Group is a part of the Institute of Informatics of Warsaw University. The group participated in the previous TYPES project Computer-Assisted Reasoning based on Type Theory in 1999-2003.

The expertise of the group as a whole is mostly in logics of programs, typed lambda calculi, type inference, finite model theory, theory of tree automata and mu calculus. Recently there is a growing interest towards proof assistants, especially the Coq system. This has already resulted in two PhD works prepared in collaboration with Paris Sud.

The group plans to contribut to the following objectives of this proposal.


work on inductive definitions, subtyping, termination, rewriting and modules.

Correctness of computer systems

work on programming with dependent types.

Formal mathematics and education

case studies.

We plan to continue and expand the collaboration with Paris Sud, INRIA and other sites, including possible further joint PhD projects.

The members of the group who will participate in the project include:

Warsaw homepage

Bengt Nordström 2005-09-22