Reasoning about contextual equivalence: From untyped to polymorphically typed Calculi

Abstract: 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. 1