Sciweavers

Share
GI
2009
Springer

Reasoning about Contextual Equivalence: From Untyped to Polymorphically Typed Calculi

11 years 4 months ago
Reasoning about Contextual Equivalence: From Untyped to Polymorphically Typed Calculi
: This paper describes a syntactical method for contextual equivalence in polymorphically typed lambda-calculi. Our specific calculus has letrec as cyclic let, data constructors, case-expressions, seq, and recursive types. The typed language is a subset of the untyped language. Normal-order reduction is defined for the untyped language. Since there are less typed contexts the typed contextual preorder and equivalence are coarser than the untyped ones. We use type-labels for all subexpressions of the typed expressions, and prove a context lemma for the type-labeled calculus. We show how to reason about correctness of program transformations in the typed language, and how to easily transfer the methods and results from untyped program calculi to polymorphically typed ones.
David Sabel, Manfred Schmidt-Schauß, Frederi
Added 24 Jul 2010
Updated 24 Jul 2010
Type Conference
Year 2009
Where GI
Authors David Sabel, Manfred Schmidt-Schauß, Frederik Harwath
Comments (0)
books