Previous: Udine
Warsaw
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.
Foundations
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:
- Pawe Urzyczyn, contact person
- Jerzy Tiuryn
- Aleksy Schubert
- Daria Walukiewicz-Chrzaszcz
- Jacek Chrzaszcz
- Zdzisaw Spawski (afilliated with Wrocaw University of Technology)
Bengt Nordström 2005-09-22