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

Slightly expanded version available as Postscript(252 KB) or gzip'ed Postscript (94 KB)

BibTeX Entry

@InProceedings{PR:99, author = "Holger Pfeifer and Harald Rueß", title = "{Polytypic Proof Construction}", editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and and L. Théry", series = "Lecture Notes in Computer Science", number = "1690", pages = "55--72", booktitle = "Proc. 12th Intl. Conf. on Theorem Proving in Higher Order Logics", year = 1999, publisher = "Springer-Verlag", month = sep }