Abstract
This paper deals with formalizations and verifications in type theory that are abstracted with respect to a class of datatypes; i.e poly-typic 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.
Cite
CITATION STYLE
Pfeifer, H., & Rueß, H. (1999). Polytypic proof construction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1690, pp. 55–72). Springer Verlag. https://doi.org/10.1007/3-540-48256-3_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
