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

@article{JV09, 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.}, author = {Johann, Patricia and Voigtl\"{a}nder, Janis}, citeulike-article-id = {5202219}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.ic.2007.11.009}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/S0890540108001314}, citeulike-linkout-2 = {http://wwwtcs.inf.tu-dresden.de/~voigt/iandc.pdf}, doi = {10.1016/j.ic.2007.11.009}, issn = {08905401}, journal = {Information and Computation}, keywords = {call-by-name, deforestation, errors, free-theorems, functional-programming, haskell, lambda-calculus, lazy-evaluation, logical-relations, operational-semantics, parametricity, polymorphism, program-transformation, rank-2, selective-strictness, seq, shortcut-deforestation, types}, month = {February}, number = {2}, pages = {341--368}, posted-at = {2009-07-19 07:38:42}, priority = {0}, publisher = {Elsevier}, title = {A family of syntactic logical relations for the semantics of Haskell-like languages}, url = {http://dx.doi.org/10.1016/j.ic.2007.11.009}, volume = {207}, year = {2009} }

TY - JOUR ID - JV09 L3 - citeulike-article-id:5202219 N2 - 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. IS - 2 JF - Information and Computation SN - 08905401 EP - 368 TI - A family of syntactic logical relations for the semantics of Haskell-like languages PB - Elsevier VL - 207 SP - 341 KW - call-by-name KW - deforestation KW - errors KW - free-theorems KW - functional-programming KW - haskell KW - lambda-calculus KW - lazy-evaluation KW - logical-relations KW - operational-semantics KW - parametricity KW - polymorphism KW - program-transformation KW - rank-2 KW - selective-strictness KW - seq KW - shortcut-deforestation KW - types AU - Johann, Patricia AU - Voigtländer, Janis PY - 2009/02// UR - http://dx.doi.org/10.1016/j.ic.2007.11.009 ER -