Up: Cooperating sites
This site includes mathematics and computer science groups at Ludwig-Maximilians-Universität, München. The site is very strong in logic and foundations, especially proof theory (and its application to computer programs), semantics of dependent types, and feasible and resource-limited computation. The MINLOG interactive proof system has been developed by this site. The site has been a part of several previous EU TYPES projects, and has a joint PhD programme ``Logic in Computer Science'' with the TU München site (financed by the German Research Foundation).
The site plans to contribute to the objectives of this proposal mainly in the following areas. <
Correctness of Computer Systems
The site collaborates with Edinburgh on Mobile Resource Guarantees. There is work on justification of programming language concepts inspired from proof theory, such as continuations, and on specification and verification of functional programs with higher-order inductive and coinductive datatypes.
Formal Mathematics and Mathematics Education
Work on formal topology within type theory, and on mathematics education using the Minlog Proof Checker.
Ongoing work includes type based termination, program development by proof transformation, program extraction from classical proofs and program extraction by realizability interpretation. Also of interest are intensional behaviour of datatypes, expressiveness of fragments of polymorphic lambda calculus and representation of binding syntax by nested datatypes.
The key members involved are
- Helmut Schwichtenberg, contact person
- Andreas Abel
- Klaus Aehlig
- Wilfried Buchholz
- Martin Hofmann
- Hans-Wolfgang Loidl
- Ralph Matthes
- Peter Schuster
- Olha Shkaravska
Bengt Nordström 2005-09-22