Strathprints logo
Strathprints Home | Open Access | Browse | Search | User area | Copyright | Help | Library Home | SUPrimo

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)

Abstract

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.

Item type: Article
ID code: 19245
Keywords: logical relations, reasoning, language programs, parametric polymorphism, observational behavior, polymorphic calculi, Electronic information resources, Computational Theory and Mathematics, Theoretical Computer Science, Information Systems, Computer Science Applications
Subjects: Bibliography. Library Science. Information Resources > Information resources > Electronic information resources
Department: Faculty of Science > Computer and Information Sciences
Related URLs:
    Depositing user: Strathprints Administrator
    Date Deposited: 14 Jun 2010 14:21
    Last modified: 05 Sep 2014 03:14
    URI: http://strathprints.strath.ac.uk/id/eprint/19245

    Actions (login required)

    View Item