×

Towards patterns for heaps and imperative lambdas. (English) Zbl 1355.68040

Summary: 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, O. de Moor and J. Gibbons [Lect. Notes Comput. Sci. 1816, 371–390 (2000; Zbl 0983.68042)] 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.

MSC:

68N18 Functional programming and lambda calculus

Citations:

Zbl 0983.68042

Software:

Toolchain
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Appel, Andrew W., Program Logics for Certified Compilers (2014), Cambridge University Press · Zbl 1298.68009
[2] Bird, Richard; de Moor, Oege, Algebra of Programming (1996), Prentice Hall · Zbl 0847.68014
[4] Carl Backhouse, Roland; Jansson, Patrik; Jeuring, Johan; Meertens, Lambert G. L.T., Generic programming: an introduction, (Advanced Functional Programming (1998)), 28-115
[5] Banerjee, Anindya; Naumann, David A., Ownership confinement ensures representation independence for object-oriented programs, J. ACM, 52, 6, 894-960 (2005) · Zbl 1316.68033
[6] Banerjee, Anindya; Naumann, David A., State based encapsulation for modular reasoning about behavior-preserving refactorings, (Clarke, Dave; Noble, James; Wrigstad, Tobias, Aliasing in Object-oriented Programming. Aliasing in Object-oriented Programming, Springer State-of-the-art Surveys, vol. 7850 (2012))
[7] Banerjee, Anindya; Naumann, David A.; Rosenberg, Stan, Local reasoning for global invariants, part I: Region logic, J. ACM, 60, 3, 18:1-18:56 (2013) · Zbl 1281.68154
[8] Bunkenburg, Alex, Expression refinement (1997), University of Glasgow, Dissertation
[9] Back, Ralph-Johan; von Wright, Joakim, Refinement Calculus: A Systematic Introduction (1998), Springer-Verlag · Zbl 0949.68094
[10] de Moor, Oege, An exercise in polytypic programming: repmin (September 1996), (accessed June 2015)
[11] Dang, Han-Hing; Moeller, B., Extended transitive separation logic, J. Log. Alg. Meth. Prog., 84 (2015) · Zbl 1330.03071
[12] de Moor, Oege; Gibbons, Jeremy, Pointwise relational programming, (Algebraic Methodology and Software Technology. Algebraic Methodology and Software Technology, Lect. Notes Comput. Sci., vol. 1816 (2000)), 371-390 · Zbl 0983.68042
[13] Freyd, Peter J.; Scedrov, Andre, Categories, Allegories (1990), North-Holland · Zbl 0698.18002
[14] Gardiner, Paul H. B.; Martin, Clare E.; de Moor, Oege, An algebraic construction of predicate transformers, Sci. Comput. Program., 22, 21-44 (1994) · Zbl 0807.18003
[15] Gunter, Carl A., Semantics of Programming Languages (1992), MIT · Zbl 0823.68059
[16] Hoogendijk, Paul; de Moor, Oege, Container types categorically, J. Funct. Program., 10, 2, 191-225 (2000) · Zbl 0959.68023
[17] Hinze, Ralf, Constructing tournament representations: an exercise in pointwise relational programming, (Mathematics of Program Construction. Mathematics of Program Construction, Lect. Notes Comput. Sci., vol. 2386 (2002)), 131-147 · Zbl 1073.68578
[18] Hoare, Tony; van Staden, Stephan; Möller, Bernhard; Struth, Georg; Villard, Jules; Zhu, Huibiao; O’Hearn, Peter W., Developments in concurrent Kleene algebra, (Relational and Algebraic Methods in Computer Science (RAMiCS). Relational and Algebraic Methods in Computer Science (RAMiCS), Lect. Notes Comput. Sci., vol. 8428 (2014)), 1-18 · Zbl 1344.68148
[19] Morris, Joseph M.; Bunkenburg, Alexander; Tyrrell, Malcolm, Term transformers: a new approach to state, ACM Trans. Program. Lang. Syst., 31, 4 (2009)
[20] Martin, Clare E.; Curtis, Sharon A., Monadic maps and folds for multirelations in an allegory, (Unifying Theories of Programming, Second International Symposium, Revised Selected Papers. Unifying Theories of Programming, Second International Symposium, Revised Selected Papers, Lect. Notes Comput. Sci., vol. 5713 (2008)), 102-121 · Zbl 1286.68087
[21] Martin, Clare E.; Curtis, Sharon A.; Rewitzky, Ingrid, Modelling angelic and demonic nondeterminism with multirelations, Sci. Comput. Program., 65, 2, 140-158 (2007) · Zbl 1106.68023
[22] Martin, C. E.; Hoare, C. A.R.; He, Jifeng, Pre-adjunctions in order enriched categories, Math. Struct. Comput. Sci., 1, 141-158 (1991) · Zbl 0755.18003
[23] Morgan, Carroll, Programming from Specifications (1994), Prentice Hall · Zbl 0829.68083
[24] Morris, Joseph M.; Tyrrell, Malcolm, Dually nondeterministic functions, ACM Trans. Program. Lang. Syst., 30, 6 (2008)
[25] Morris, Joseph M.; Tyrrell, Malcolm, Modelling higher-order dual nondeterminacy, Acta Inform., 45, 6, 441-465 (2008) · Zbl 1160.68006
[26] Naumann, David A., Beyond Fun: order and membership in polytypic imperative programming, (Mathematics of Program Construction. Mathematics of Program Construction, Lect. Notes Comput. Sci., vol. 1422 (1998)), 286-314
[27] Naumann, David A., A categorical model for higher order imperative programming, Math. Struct. Comput. Sci., 8, 4, 351-399 (1998) · Zbl 0916.68095
[28] Naumann, David A., Towards squiggly refinement algebra, (Gries, David; de Roever, Willem-Paul, Programming Concepts and Methods (1998), Chapman and Hall), 346-365
[29] Naumann, David A., Ideal models for pointwise relational and state-free imperative programming, (Principles and Practice of Declarative Programming (2001)), 4-15
[30] Nanevski, Aleksandar; Morrisett, J. Gregory; Birkedal, Lars, Hoare type theory, polymorphism and separation, J. Funct. Program., 18, 5-6, 865-911 (2008) · Zbl 1155.68354
[31] Oliveira, José Nuno, Extended static checking by calculation using the pointfree transform, (Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School, Revised Tutorial Lectures. Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School, Revised Tutorial Lectures, Lect. Notes Comput. Sci., vol. 5520 (2009)), 195-251 · Zbl 1250.68093
[32] Wang, Shuling; Soares Barbosa, Luís; Nuno Oliveira, José, A relational model for confined separation logic, (International Symposium on Theoretical Aspects of Software Engineering (TASE) (2008)), 263-270
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.