Logic and Computation
This very general project deals with the close connections between mathematical logic and certain parts of computer science, and emphasis is put on a proof-theoretic approach to some of the central questions in this area of research. These include the development of perspicuous and feasible logical frameworks for studying typical questions in computer science like termination and correctness of functional programs, properties of distributed systems and the like.
We study applicative theories as well as strongly typed formalisms and are interested in the connections to constructive and explicit mathematics. Furthermore, we are interested in analyzing the close connections between the complexities of computations and proofs in suitable formalizations, ranging from propositional calculi up to abstract frameworks for computations (in higher types).
Staff: All members of the group.
