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):
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!
Last modified: February 28, 2013
Responsible for this page: Peter Dybjer