Polytypic Proof Construction

Presented at the 12th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'99. Springer LNCS, Vol. 1690, Sept. 1999, © Springer-Verlag.

---

Authors

Holger Pfeifer and Harald Rueß

Abstract

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.

gzipped postscript or postscript

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
 }

---

Harald Ruess: ruess@csl.sri.com