Programming Logic Group
The Programming Logic group develops methods, tools and theories for constructing provably correct software. A central theme is the idea of a logical framework for programming: a unified theory of formal systems in which many different logical systems can be conveniently expressed. Such a framework can be implemented and equipped with a state of the art window interface, thus providing a convenient proof development environment for a range of different applications.
We work on the following subprojects (with principal investigator):
- Typed Lambda Calculus and Applications (Peter Dybjer)
- Type Theory and Computational Mathematics (Thierry Coquand)
- Proof Editors (Bengt Nordström)
- Automated Theorem Proving in Type Theory (Catarina Coquand)
- Formalising General Recursion in Type Theory (Ana Bove)
- Type Theory and Natural Language Technology (Aarne Ranta)
- Generic Programs and Proofs (Patrik Jansson)
Our work can be characterized by the close interaction between theory, experiments and implementation work. The basic source of inspiration for our theoretical work lies in Martin-Löf's theory of types and Coquand's calculus of constructions. We have many implementations of different versions of these languages. Using the implementations we have made experiments in developing formal proofs in the field of programming, topology and metamathematics. These experiments have given us new ideas about how a logic should be built up. This has led us to theoretical investigations and new implementations. But the implementation work has also a direct effect on theory; our earlier typechecker was too complicated and forced us to design a new language.
We feel privileged to work in a new subject like Computing Science, where both experiments and theoretical work can take place in one single research group!
HISTORY
The Programming Methodology Group (PMG) in Gothenburg was formed in 1980, as a group of people interested in semantically simple, clean and powerful languages. From this common philosophy three major strands of research developed: programming logics and Martin-Löf's theory of types; functional programming languages, their use and implementation; and process calculi such as CCS. Although the research has diversified, we still share the common goal of developing tools and methodologies for deriving correct as well as efficient programs.