In today's society, many critical systems are controlled by computers: transportation safety, medical devices, commerce and public communication. The software that runs on those computers, however, is often developed on weak foundations, which regularly causes it to behave in unanticipated and rather undesirable ways.

  To develop the software we can rely on, based on solid logical and mathematical foundations, we study programming languages, methods, tools and computational models. Our recent research topics include:

Proof techniques for program equivalence: The fundamental question underlying program optimization and transformation is whether two programs behave the same. We have developed an “environment bisimulation” technique for proving program equivalence and applied it to a wide range of programming languages and computational models.

Functional programming: Functional programming is gaining interest as a reliable, easy to reason and powerful programming method. Helping raise this interest is the annual international programing contest, with world-wide participation by top-level programmers and researchers. We have served as the organizers of the 2011 programming contest.

Bidirectional transformation: In today's distributed world, we often have to keep many sets of data in sync: transforming from one set to another and back. We are developing programming languages and techniques for correct-by-construction bidirectional transformations.