Research Program

Center
The program seeks to identify programming patterns (program methodology), to formalize them in the form of well defined programming languages and language constructs, and to support their use by the construction of tools. When constructing the tools we reflect about the way we construct these tools, thus closing the development cycle by identifying new patterns. 

The leading principle in this cycle is  _compositionality_ : the only way to more efficient software construction is by composing software out of smaller, well understood, formalized and well tested components.  

When composing components we need to check whether they can be composed at all, and thus a formal specification of the interfaces is needed. We define the _type_ of a component as the specification of this interface; the type system used for an interface can range from very simple syntactic approaches as e.g. in Java, to a complete specification of the full semantics of a component using dependent types.  

To express oneself at an level as high as possible a component  should be a first class citizen, meaning that it can play the role of an argument , that it can be returned as result and that the same holds for the composition mechanisms themselves. In this way the abstraction level at which actual programming takes place can be raised to the point where we also can compose composition mechanisms. So besides composition mechanisms we also try to exploit _abstraction mechanisms_. 

Currently lazy evaluated, strongly typed functional languages provide the most fertile starting point for this line of research; first-classness is a leading design principle in those languages, and it is here that we find,  amongst the practical programming languages, the most advanced type systems . As a result we have focussed a large part of our research around the language Haskell. If possible we try to formalize our patterns using Haskell itself, because in that way we automatically inherit  powerful typing and abstraction mechanisms. If this fails, we have developed tools that can be used to analyze and transform programs from the abstract into the concrete form.

The explicit use of advanced type systems is cumbersome for the everyday programmer, with as an extreme the need to provide a complete formal proof of the program. Fortunately a lot of this work can be avoided by having tools  that automatically infer a lot of  essential information. Examples of this are type inferencing in functional languages and the use of proof-tactics when using theorem provers. One of the problems that arises when using these tools is when the analyzed components are incorrect or incompatible. In this case a long calculation may fail to construct a proof, but it may be far from clear where the source of the error is located. The question of how to report inconsistencies or incompleteness resulting from global program analyses and abstract interpretations back in terms of the constructs used at the higher abstraction levels is still an open problem, of which the surface has only been scratched.  

Where possible we try to incorporate our results in advanced courses, so students can actively participate in the research we are doing. Furthermore the software we develop is made available through our website and version management systems.