Formal Models of Computation

Programming Language Design
Substructural Type Systems: linear and affine calculi, defined by substructural type systems, have several known advantages (typable in polynomial type, implementation with updates in place, no need of garbage collection). But these calculi are not expressive enough to write useful programs. Previously, researchers from this group defined simple extensions to these substructural systems based on explicit iteration, and showed that it is possible to compile non linear calculi into these new calculi. They also showed that these new calculi are quite expressive. One of our goals now, is the extensions of the previous compilation to Turing complete languages based on recursion. This will have a larger impact on programming language technology. Another goal is the definition of suitable linear type systems for these new linear versions based on recursion. This has some research challenges related to decidable typability of recursion.
Program Analysis and Program Transformation: strictness analysis is a relevant area in the implementation of lazy functional programming languages. Previous analysis are mostly based on abstract interpretation. Our goal is to simplify previous methods by using program transformation techniques before the analysis so that the abstract domain becomes simpler. This work will have a general impact in the area of strictness analysis and a particular application in another line of research of this group related with resource analysis. [More info]

Proof Theory
Provability in implicational fragments of intuitionistic logic is equivalent to inhabitation of types in systems of typed lambda-calculus. Implicational formulas and  types are syntactically identical and by the Curry-Howard isomorphism every (normal) inhabitant of a type tau may be regarded as a (normal) proof of the formula tau. Previously, researchers of this group defined the Formula-Tree Proof Method, which is a method for investigating inhabitation in the system of simple types, which lies at the core of nearly every functional programming language. Research in this area focuses on extensions and applications of this method and other type-theoretic techniques in the field of type/proof-theory.  [More info]

Program Verification
Tools and techniques for the formal verification of computer systems. We are interested in providing tools and design techniques for the formal verification in the large. We are particularly interested in the Design by Contract approach, specification transforming techniques (like refinement and abstraction) and the use of proof assistants like COQ in such a context.  
Applications of formal verification tools and techniques: we are interested in applying these tools for the formal verification of safety critical systems like electronic voting systems, smart card based information systems etc.
Resource analysis: effect types have been used to describe intentional aspects of program behaviour, such as side effects, communication analysis or resource analysis (time and space). Previous research in LIACC used type and effect systems for resource analysis of a strict functional language. Our goal is to define a type and effect system for resource analysis of a lazy functional programming language. The lazy case is more complex because dynamic behaviour of programs is rather difficult to predict. But results in this area will have a great impact in the use of standard lazy declarative languages (Haskell) in resource bounded domains such as embedded and critical systems. [More info]