Gesellschaft fr Informatik e.V.

Lecture Notes in Informatics

INFORMATIK 2009 - Im Focus das Leben P-154, 2931-2945 (2008).

Gesellschaft für Informatik, Bonn


Stefan Fischer, Erik Maehle, Rüdiger Reischuk (eds.)

Copyright © Gesellschaft für Informatik, Bonn


Reasoning about contextual equivalence: from untyped to polymorphically typed calculi

David Sabel , Manfred Schmidt-Schauß and Frederik Harwath


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. Using type-labels for all subexpressions of the typed expressions, 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.

Full Text: PDF

Gesellschaft für Informatik, Bonn
ISBN 978-3-88579-241-3

Last changed 24.01.2012 22:11:12