TY - JOUR
T1 - Towards patterns for heaps and imperative lambdas
AU - Naumann, David A.
N1 - Publisher Copyright:
© 2015 Elsevier Inc.
PY - 2016/8/1
Y1 - 2016/8/1
N2 - In functional programming, pointfree relation calculi have been fruitful for general theories of program construction, but for specific applications pointwise expressions can be more convenient and comprehensible. In imperative programming, refinement calculi have been tied to pointwise expression in terms of state variables, with the curious exception of the ubiquitous but invisible heap. To integrate pointwise with pointfree, de Moor and Gibbons [12] extended lambda calculus with non-injective pattern matching interpreted using relations. This article gives a semantics of that language using “ideal relations” between partial orders, and a second semantics using predicate transformers. The second semantics is motivated by its potential use with separation algebra, for pattern matching in programs acting on the heap. Laws including lax beta and eta are proved in these models and a number of open problems are posed.
AB - In functional programming, pointfree relation calculi have been fruitful for general theories of program construction, but for specific applications pointwise expressions can be more convenient and comprehensible. In imperative programming, refinement calculi have been tied to pointwise expression in terms of state variables, with the curious exception of the ubiquitous but invisible heap. To integrate pointwise with pointfree, de Moor and Gibbons [12] extended lambda calculus with non-injective pattern matching interpreted using relations. This article gives a semantics of that language using “ideal relations” between partial orders, and a second semantics using predicate transformers. The second semantics is motivated by its potential use with separation algebra, for pattern matching in programs acting on the heap. Laws including lax beta and eta are proved in these models and a number of open problems are posed.
UR - http://www.scopus.com/inward/record.url?scp=85010917057&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85010917057&partnerID=8YFLogxK
U2 - 10.1016/j.jlamp.2015.10.008
DO - 10.1016/j.jlamp.2015.10.008
M3 - Article
AN - SCOPUS:85010917057
VL - 85
SP - 1038
EP - 1056
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
IS - 5
ER -