Functional-Logic Development and Implementation Techniques

Research Group
Functional-Logic Development
& Implementation Techniques

Peter Padawitz
office hour by appointment

read - - - laugh - - - cry!

Painter:
Haskell-Funktionen zur graphischen Wiedergabe und Animation von Texten, Bäumen, Graphen, Fraktalen, etc. - zur Visualisierung von Auswertungen und Reduktionen von Termgraphen sowie anderen Transformationen zweidimensionaler Figuren, auch der mit Expander2 erstellten, z.B. von
Penrose-Tilings

Invited paper:
From grammars and automata to algebras
and coalgebras
(Proc. CAI 2011)

Campusfest 2010:
Vortrag über funktionale Programmierung

Research topics
& projects

• 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 have called them 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, Jos Kusiek, Jens Lechner, Hubert Wagner)

• 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, Jos Kusiek, Sebastian Venier, Karsten Lettow, Jochen Gerlach, Marcel Köppen, Markus Heller)

• Classical and non-classical logics in computer science (Hubert Wagner, Peter Padawitz)

• Hyperdocument design with formal methods (Volker Mattick, Oliver Geppert, Peter Padawitz)

• 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, Jos Kusiek, Pascal Hof, 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)

• My current research & development is here (click vertices of the pentagon)