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)
• QuickProof - a system for specification driven software development (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!