Polytypic programming in Maude.

*(English)*Zbl 0962.68030
Futatsugi, Kokichi, The 3rd international workshop on rewriting logic and its applications, RWLW. Kanazawa City Cultural Hall, Kanzawa, Japan, September 18-20, 2000. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 36, 22 p., electronic only (2000).

Summary: The idea of polytypic programming is to write programs that are defined by induction on the structure of user-defined datatypes. In this way, many functions with similar functionalities do not have to be written over and over again for different datatypes. So far, this programming style has been developed in functional languages like Haskell, extended with new syntactic constructs for defining polytypic programs. In this paper we show that polytypic programming can be reduced to metaprogramming, and that can be developed in a reflective first-order language like Maude, without having to extend the language. This has the additional advantage of allowing us to use standard formal tools to prove properties about polytypic programs. We illustrate our methodology via examples. In particular, we explain how to define in Maude two non-trivial generic functions, namely, the polytypic versions of the functions map and cata, and how to prove properties about them using an inductive theorem prover for Maude modules.

For the entire collection see [Zbl 0957.00046].

For the entire collection see [Zbl 0957.00046].

##### MSC:

68N19 | Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) |

68Q42 | Grammars and rewriting systems |

68Q60 | Specification and verification (program logics, model checking, etc.) |