Prof. Dr. Peter Padawitz This email address is being protected from spambots. You need JavaScript enabled to view it. +49-231-755-5108 Room 3.021 Contact
Dipl.-Inf. Jos Kusiek This email address is being protected from spambots. You need JavaScript enabled to view it. +49-231-755-7523 Room 3.020 Contact


  • Development of a uniform framework for the integrated specification and verification of constructor-based visible types on the one hand and state-based hidden types on the other hand. We call them dialgebraic or swinging types and use them in various application areas, in particular those where - traditionally - modal logic or object-oriented programming plays the major rôle. The semantics of swinging types is given by Herbrand models with least and greatest relational fixpoints. Proofs about swinging types make heavy use of induction and coinduction. (Peter Padawitz)
  • The prototyping system Expander2 is a multi-purpose workbench for interactive logical inference, constraint solving, data flow analysis and other rule-based manipulations of algebraic terms, logical formulas and graphical representations thereof, which range from term graphs to various turtle-system-generated pictures Expander2 has been written in O'Haskell, an extension of Haskell with object-oriented features for reactive programming and a typed interface to Tcl/Tk for developing GUIs. Besides a comfortable GUI the design goals of Expander2 were to integrate testing, proving and visualizing deductive methods, to admit several degrees of interaction and to keep the system open for extensions or adaptations of individual components to changing demands. Proofs and computations performed with Expander2 follow the rules and the semantics of swinging types. (Peter Padawitz, Sebastian Venier, Karsten Lettow, Jochen Gerlach, This email address is being protected from spambots. You need JavaScript enabled to view it., Markus Heller)
  • Classical and non-classical logics in computer science (Hubert Wagner)
  • Hyperdocument design with formal methods (Volker Mattick, Oliver Geppert)
  • Case studies in functional programming with Haskell and ML, functional programming with reactive objects (O'Haskell), functional-logic programming (Curry) and rewriting-logic programming (Maude) (Peter Padawitz, Karsten Lettow, Jochen Gerlach, Matthias Hellwig, Hartmut Kahl) See also The Journal of Functional and Logic Programming and WFLP 2006 - 15th Workshop on Functional and (Constraint) Logic Programming
  • Design and verification of algebraic Petri nets; translation of SDL systems into LOTOS processes and algebraic nets - in cooperation with TÜV Informationstechnik (Oliver Niese, Peter Padawitz)
  • Konzeption und Koordination der Mathematikausbildung und -anwendung: Teilprojekt V.2 des Sofortprogramms Weiterentwicklung des Informatikstudiums an den deutschen Hochschulen; 2001-2003 (Volker Mattick, Peter Padawitz)

Weitergehende Informationen: