A Family Of Syntactic Logical Relations For The Semantics Of Haskell-Like Languages
- ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
- Patricia Johann Ph.D, Professor (Creator)
- Institution
- Appalachian State University (ASU )
- Web Site: https://library.appstate.edu/
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 over 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 ?ne-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 de?nedness 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.
A Family Of Syntactic Logical Relations For The Semantics Of Haskell-Like Languages
PDF (Portable Document Format)
412 KB
Created on 4/25/2016
Views: 1428
Additional Information
- Publication
- Patricia, Johann; Janis, Voigtlaender. (2009) "A Family of Syntactic Logical Relations for the Semantics of Haskell-Like Languages". Information and Computation, vol. 207, no. 2, pp. 341 - 368. (ISSN: 0890-5401) Version Of Record Available At www.sciencedirect.com
- Language: English
- Date: 2009
- Keywords
- syntax, haskell, semantics, syntactic logical relations