Picture of two heads

Open Access research that challenges the mind...

The Strathprints institutional repository is a digital archive of University of Strathclyde research outputs. Strathprints provides access to thousands of Open Access research papers by University of Strathclyde researchers, including those from the School of Psychological Sciences & Health - but also papers by researchers based within the Faculties of Science, Engineering, Humanities & Social Sciences, and from the Strathclyde Business School.

Discover more...

A family of syntactic logical relations for the semantics of Haskell-like languages

Johann, Patricia and Voigtlander, Johann (2009) A family of syntactic logical relations for the semantics of Haskell-like languages. Information and Computation, 207 (2). pp. 341-368. ISSN 0890-5401

Full text not available in this repository. (Request a copy from the Strathclyde author)


Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming language features have been introduced in recent years. Unfortunately, the calculi studied are typically idealized, and the results obtained for them offer only partial insight into the impact of such features on observational behavior in implemented languages. In this paper, we show how to bring reasoning via logical relations closer to bear on real languages by deriving results that are more pertinent to an intermediate language for the (mostly) lazy functional language Haskell like GHC Core. To provide a more fine-grained analysis of program behavior than is possible by reasoning about program equivalence alone, we work with an abstract notion of relating observational behavior of computations which has among its specializations both observational equivalence and observational approximation. We take selective strictness into account, and we consider the impact of different kinds of computational failure, e.g., divergence versus failed pattern matching, because such distinctions are significant in practice. Once distinguished, the relative definedness of different failure causes needs to be considered, because different orders here induce different observational relations on programs (including the choice between equivalence and approximation). Our main contribution is the construction of an entire family of logical relations, parameterized over a definedness order on failure causes, each member of which characterizes the corresponding observational relation. Although we deal with properties very much tied to types, we base our results on a type-erasing semantics since this is more faithful to actual implementations.