Prof. Dr. Peter Padawitz

address: Informatik 1, Technische Universität Dortmund

D-44227 Dortmund, Germany
phone: +49 231 755 5108
secretary: +49 231 755 6223
fax: +49 231 755 6555

Research, Projects, Courses     Systems     Papers     Books     Vita


A Formal Methods Presenter and Animator
Having started as the successor of Expander (see below), Expander2 shall evolve to a multi-purpose workbench for interactive logical inference, constraint solving, data flow analysis, rewriting logic and related procedures building up proofs or computation sequences. Moreover, several interpreters translate expressions into tailor-made two-dimensional representations that range from trees and term graphs to tables, fractals and other turtle-system-generated pictures.

Expander2 is equipped with a GUI that permits the user to interact with the system at three levels of decreasing control over proofs and computations. At the first level, rules like induction and coinduction are applied locally and step by step. At the second level, goals are rewritten or narrowed, i.e. axioms are applied exhaustively and iteratively. At the third level, built-in rules (some of them execute Haskell programs) simplify, i.e. (partially) evaluate terms and formulas, and thus hide routine steps of a proof or computation.

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. Besides a comfortable GUI the design goals of Expander2 were to integrate testing, proving and visualizing deductive methods, admit several degrees of interaction and 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. Swinging types combine constructor-based visible types with state-based hidden ones and have unique Herbrand models that interpret relations as the least or greatest solutions of their axioms.

Expander: A System for Testing and Verifying Functional-Logic Programs
83 pages; last update: June 2, 1996

Expander is a proof and test environment for algebraic data type specifications and functional-logic programs. Program design, test and verification are supported by tailor-made deduction rules for proving Gentzen clauses, which are the most frequently used formulas for expressing requirements and queries to data types. Inductive proofs are built up from simplification, subsumption, resolution, rewriting and narrowing steps in a natural way that permits interaction on various levels. The core system is written in Standard ML. User interfaces are available for NeXTSTEP and X.

Contents: 1 A uniform proof method - 2 Design language - 3 Rules - 4 Commands - 5 Built-in simplifications - 6 Error messages - 7 Sample proofs and tests - 8 Source code (the pure code listing starts on page 40)
see The Expander Page

Papers and talks

I-polynomial data types: adjunctions, equations, and theories
CMCS 2016
Modeling and reasoning with I-polynomial data types
Eindhoven IFIP WG1.3 meeting (March 31 - April 1, 2016)
Many-sorted (Co)Algebraic Specification with Base Sets, Recursive and Iterative Equations
Theddingworth IFIP WG1.3 meeting (January 7-10, 2014)
Many-sorted signatures presenting categories of co/algebras
Winchester IFIP WG1.3 meeting (September 3-4, 2011)
From grammars and automata to algebras and coalgebras (invited lecture)
Proc. CAI 2011, Springer LNCS 6742 (2011) 21-43; revised version
slides for the lecture and the accompanying tutorial
Algebraic model checking in: Electronic Communications of the EASST Vol. 26 (2010)
detailed slides on this and related topics
Algebraic compilers and their implementation in Haskell actualized slides
Sierra Nevada IFIP WG1.3 meeting (January 14-18, 2008)
Mehrpässige Compilation mit finalen Coalgebren actualized slides
in: Proc. 14. Kolloquium "Programmiersprachen und Grundlagen der Programmierung", Universität Lübeck (2007) 
Expander2: Program Verification Between Interaction and Automation (invited lecture) actualized version
in: F.J. Lopez Fraguas, ed., Proc. 15th Workshop on Functional and (Constraint) Logic Programming, Elsevier ENTCS 177 (2007) 35-57 
Expander2: Towards a Workbench for Interactive Formal Reasoning (invited paper)
in: H.-J. Kreowski, U. Montanari, F. Orejas, G. Rozenberg, G. Taentzer, eds., Formal Methods in Software and System Modeling, Springer LNCS 3393 (2005) 236-258 
Dialgebraic Specification and Modeling
see The Swinging World
(1) Swinging Types = Functions + Relations + Transition Systems A4 format letter format
Theoretical Computer Science 243 (2000) 93-165
see The Swinging World
(2) Swinging Types At Work A4 format letter format
see The Swinging World
Structured Swinging Types
see The Swinging World
Basic Inference Rules for Algebraic and Coalgebraic Specifications A4 format letter format
see The Swinging World
Swinging UML: How to Make Class Diagrams and State Machines Amenable to Constraint Solving and Proving
Proc. UML 2000, Springer LNCS 1939 (2000) 162-177
Integrating Functional-Logic and State-Oriented Specifications A4 format letter format
Int. Workshop on Functional-Logic Programming, Grenoble 1999 (invited lecture)
28 pages; last update: September 1, 1999
The paper summarizes basic issues about the syntax, semantics and proof theory of swinging types that were developed for specifying and verifying "static" data types and dynamic systems within a uniform logic. More details and all proofs can be found in (1). More applications are given in (2).
Towards the One-Tiered Design of Data Types and Transition Systems
Proc. WADT'97, Springer LNCS 1376 (1998) 365-380
The paper includes a preliminary version of the coinductivity criterion for behaviorally consistent specifications given in (1)
(3) Swinging Data Types: The dialectic between actions and constructors
see The Swinging World
Swinging Data Types: Syntax, Semantics, and Theory
Proc. WADT'95, Springer LNCS 1130 (1996) 409-435
short version of Chapters 1 to 5 of (3)
Proof in Flat Specifications A4 format letter format
in: E. Astesiano, H.-J. Kreowski, B. Krieg-Brückner, eds., Algebraic Foundations of Systems Specification, IFIP State-of-the-Art Report, Springer (1999) 321-384
55 pages; last update: April 12, 1998
Contents: 10.1 Introduction - 10.2 Standard specifications - 10.3 Final semantics and bisimilarity - 10.4 Gentzen proofs and program synthesis - 10.5 Confluence and consistency - 10.6 Implicit induction - 10.7 Unfolding and explicit induction - 10.8 Goal solving
Inductive Theorem Proving for Design Specifications
J. Symbolic Computation 21 (1996) 41-99

We present a number of new results on inductive theorem proving for design specifications based on Horn logic with equality. Induction is explicit here because induction orderings are supposed to be part of the specification. We show how the automatic support for program verification is enhanced if the specification satisfies a bunch of rewrite properties, summarized under the notion of canonicity. The enhancement is due to inference rules and corresponding strategies whose soundness is implied by the specification's canonicity. The second main result of the paper provides a method for proving canonicity by using the same rules, which are applied in proofs of conjectures about the specification and the functional-logic programs it contains.

Contents: 1 Introduction - 2 Preliminaries - 3 Generic Expansion - 4 Inductive Expansion - 5 Canonical Specifications - 6 Subreductive Expansion - 7 Strong Termination and t-boundedness - 8 Narrowing - 9 Redex Selection - 10 Simplification
Computing Rectangular Dissections:
A Case Study in Deriving Functional Programs from Logical Specifications
29 pages

Logical specifications provide an abstract level of programming where programs are given as axioms defining functions and predicates on constructor-based data types. Axiomatic function definitions are transformed into functional programs, predicate definitions are compiled into logic programs. If functions are to be implemented as logic programs, they must be flattened into predicates. In this paper, we exemplify the inverse translation: predicates used as multi-valued, nondeterministic, functions are compiled into stream-generating functions, which enumerate multiple values. Generate-and-test algorithms, usually implemented as logic programs, can be realized in this way as functional programs. Our case study deals with a configuration problem. Two nondeterministic algorithms that compute rectangular dissections are specified in the functional-logic language of Expander, flattened into Prolog programs, and, alternatively, translated into ML programs, which produce streams of dissections. Besides the compilation of predicates into stream functions the case study illustrates the use of polymorphic types and higher-order functions for accomplishing well-structured and reusable software.

Building Shelf Systems:
A Case Study in Structured ML Programming

Unchecked version! Chapter 12 of Einführung ins funktionale Programmieren contains a revised version.

We present a generic functional program for loading (two-dimensional) containers with arbitrary objects, filling shelves with items of different kinds and - last not least - designing complete shelf systems. This piece of software and its development is a case study in functional programming for solving hierarchical configuration problems. Such problems require tailor-made, but nevertheless abstract and generic data models and algorithms. We claim that these are more directly realizable in a functional language than in a classical imperative language. Polymorphism, module abstraction, semantically well-founded exception handling and the problem-oriented option for static data, "lazy" structures (streams) or dynamic objects are the main concepts of functional programming we are going to use and explain in the context of our case study.


Computing in Horn Clause Theories, EATCS Monographs on Theoretical Computer Science, Vol. 16, Springer-Verlag 1988
This book presents a unifying approach to semantical concepts and deductive methods used in recursive, equational and logic programming, data type specification and automated theorem-proving. The common background is Horn logic with equality. Although this logic does not cover full first-order logic, it supplies us with a language that allows "natural" problem specifications, offers several semantical views (functional, relational, inductive, behavioural, etc.) and puts at our disposal a number of more or less special-purpose deductive methods, which can be used as rapid prototyping tools. The Horn clause calculus serves as the interface between the model-theoretic concepts of initial semantics, final semantics and internalized logic on the one hand and deductive methods based on resolution, paramodulation, reduction and narrowing on the other hand. This contrasts previous approaches, which equip each semantical concept with its own calculus or, conversely, build a particular semantics upon each deductive method. Here I start out from the Horn clause calculus and develop individual concepts, results and procedures in a way that clearly delimits their respective purposes from each other. The unifying approach also brings about new variants or generalizations of known results and admits comparable arguments in soundness and completeness proofs.
Contents: 1. Introduction - 2. Basic Notions - 3. Sample Specifications - 4. Models and Theories - 5. Resolution and Paramodulation - 6. The Relevance of Constructors - 7. Reduction - 8. Narrowing - 9. Church-Rosser Criteria
Deduction and Declarative Programming, Cambridge Tracts in Theoretical Computer Science, Vol. 28, Cambridge University Press 1992
Declarative programs consist of mathematical functions and relations and are amenable to formal specification and verification, since the methods of logic and proof can be applied to the programs in a well-defined manner. Here I emphasize verification based on logical inference rules, i.e. deduction (in contrast to model-theoretic approaches, deductive methods can be automated to some extent). My treatment of the subject differs from others in that I try to capture the actual styles and applications of programming; neither too general with respect to the underlying logic, nor too restrictive for the practice of programming. I generalize and unify results from classical theorem-proving and term rewriting to provide proof methods tailored to declarative program synthesis and verification. Detailed examples accompany the development of the methods whose use is supported by a documented prototyping system. The book can be used for graduate courses or as a reference for researchers in formal methods, theorem-proving and declarative languages.
Contents: 0. Introduction - 1. Preliminaries - 2. Guards, Generators and Constructors - 3. Models and Correctness - 4. Computing Goal Solutions - 5. Inductive Expansion - 6. Directed Expansion and Reduction 7. Implications of Ground Confluence - 8. Examples - 9. EXPANDER: Inductive Expansion in SML

Research Topics, Projects, Courses     Systems     Papers     Books