Polytypic Abstraction in Type Theory

This paper deals with formalizations and verifications in type theory that are abstracted with respect to a class of datatypes; i.e polytypic constructions. The main advantage of these developments are that they can not only be used to define functions in a generic way but also to formally state polytypic theorems and to synthesize polytypic proof objects in a formal way. This opens the door to mechanically proving many useful facts about large classes of datatypes once and for all.

Online Copy

Available as Postscript (207 KB) or gzip'ed Postscript (78 KB)

BibTeX Entry

@InCollection{PfeiferRuess:WGP98, author = "H. Pfeifer and H. Ruess", title = "Polytypic Abstraction in Type Theory", booktitle = "Workshop on Generic Programming (WGP'98)", location = "Marstrand, Sweden", month = "June", publisher = "Dept. of Computing Science, Chalmers Univ. of Technology, and Göteborg Univ.", editor = "Roland Backhouse and Tim Sheard", url = "http://www.cs.uu.nl/people/johanj/programme_wgp98.html", year = "1998" }