Several constructive type theories have been developed in order to provide a foundation for Constructive Mathematics. Each of them can be described as a functional programming language with dependent types. This latter feature allows to express program specifications as types. Therefore, that a program has a type P can be understood as that program satisfying the specification P . The task of verifying that a given expression has a certain type is decidable in those languages, which makes the languages in question a formal theory of programming. In addition, these theories provide a formal framework in which mathematical constructions can be rigorously developed.
In what follows we list several works developed by members of the group. They are classified according to three different areas of research connected with constructive type theory.