Polytypic Abstraction in Type Theory

Presented at the Workshop on Generic Programming (WGP'98), Marstrand, Sweden, June 1998.

---

Authors

Holger Pfeifer and Harald Rueß

Abstract

his paper is concerned with formalizations and verifications in type theory that are abstracted with respect to a large class of datatypes; i.e polytypic formalizations. The main advantage of these developments are that they can not only be used to polytypically define functions but also to formally state polytypic theorems and to interactively develop polytypic proofs using existing proof editors. Polytypic program and proof construction in a type-theoretic setting is exemplified by the definition of a polytypic map function and by mechanized proofs of corresponding properties such as preservation of composition and fusion theorems.

gzipped postscript or postscript

BibTeX Entry

@incollection = {PfeiferRuess:WGP98,
    author = "H. Pfeifer and H. Rue{\ss}",
    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 Techn.\ and G{\"o}teborg Univ.",
    editor = "Roland Backhouse and Tim Sheard",
    url = "http://wsinwp01.win.tue.nl:1234/WGPProceedings/Pfeifer.ps.gz",
    year = "1998"
}

---

Harald Ruess: ruess@csl.sri.com