Sciweavers

TPHOL
2003
IEEE

Applications of Polytypism in Theorem Proving

14 years 5 months ago
Applications of Polytypism in Theorem Proving
Abstract. 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.
Konrad Slind, Joe Hurd
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where TPHOL
Authors Konrad Slind, Joe Hurd
Comments (0)