Applications of Polytypism in Theorem Proving
Applications of Polytypism in Theorem Proving
Polytypic functions have mainly been studied in the context of
functional programming languages. In that setting, applications of
polytypism include elegant treatments of polymorphic equality,
prettyprinting, and the encoding and decoding of high-level datatypes
to and from low-level binary formats. In this paper, we discuss how
polytypism supports some aspects of theorem proving: automated
termination proofs of recursive functions, incorporation of
the results of metalanguage evaluation, and equivalence-preserving
translation to a low-level format suitable for propositional
methods. The approach is based on an interpretation of higher order
logic types as terms, and easily deals with mutual and nested
recursive types.
PDF