The impact of higher-order state and control effects on local relational reasoning. (English) Zbl 1323.68203
Proceedings of the 15th ACM SIGPLAN international conference on functional programming, ICFP ’10, Baltimore, MD, USA, September 27–29, 2010. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-794-3). ACM SIGPLAN Notices 45, No. 9, 143-156 (2010).
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68N18 | Functional programming and lambda calculus |
| 68Q55 | Semantics in the theory of computing |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Keywords:
biorthogonality; exceptions; first-class continuations; higher-order state; local state; observational equivalence; state transition systems; step-indexed Kripke logical relationsSoftware:
HaskellReferences:
| [1] | }}S. Abramsky, K. Honda, and G. McCusker. A fully abstract game semantics for general references. In LICS, 1998. |
| [2] | }}A. Ahmed. Semantics of Types for Mutable State. PhD thesis, Princeton University, 2004. |
| [3] | }}A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In POPL, 2009. 10.1145/1480881.1480925 |
| [4] | }}A. Appel and D. McAllester. An indexed model of recursive types for foundational proof-carrying code. TOPLAS, 23(5):657-683, 2001. 10.1145/504709.504712 |
| [5] | }}N. Benton and C.-K. Hur. Biorthogonality, step-indexing and compiler correctness. In ICFP, 2009. 10.1145/1596550.1596567 |
| [6] | }}N. Benton and N. Tabareau. Compiling functional types to relational specifications for low level imperative code. In TLDI, 2009. 10.1145/1481861.1481864 |
| [7] | }}N. Bohr. Advances in Reasoning Principles for Contextual Equivalence and Termination. PhD thesis, IT University of Copenhagen, 2007. |
| [8] | }}D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning (Technical appendix), 2010. http://www.mpi-sws.org/ dreyer/papers/stslr/ |
| [9] | }}D. Dreyer, G. Neis, A. Rossberg, and L. Birkedal. A relational modal logic for higher-order stateful ADTs. In POPL, 2010. 10.1145/1706299.1706323 |
| [10] | }}M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. TCS, 103(2):235-271, 1992. 10.1016/0304-3975(92)90014-7 · Zbl 0764.68094 |
| [11] | }}D. Friedman and C. Haynes. Constraining control. In POPL, 1985. 10.1145/318593.318654 |
| [12] | }}D. R. Ghica and G. McCusker. Reasoning about Idealized Algol using regular languages. In ICALP, 2000. |
| [13] | }}P. Johann. Short cut fusion is correct. JFP, 13(4):797-814, 2003. 10.1017/S0956796802004409 · Zbl 1111.68406 |
| [14] | }}P. Johann, A. Simpson, and J. Voigtländer. A generic operational metatheory for algebraic effects. In LICS, 2010. 10.1109/LICS.2010.29 |
| [15] | }}P. Johann and J. Voigtländer. The impact of phseq on free theorems-based program transformations. Fundamenta Informaticae, 69(1-2):63-102, 2006. · Zbl 1096.68026 |
| [16] | }}V. Koutavas and S. Lassen. Fun with fully abstract operational game semantics for general references. Unpublished, Feb. 2008. |
| [17] | }}V. Koutavas and M. Wand. Small bisimulations for reasoning about higher-order imperative programs. In POPL, 2006. 10.1145/1111037.1111050 |
| [18] | }}J.-L. Krivine. Classical logic, storage operators and second-order lambda-calculus. Annals of Pure and Applied Logic, 68:53-78, 1994. · Zbl 0814.03009 |
| [19] | }}J. Laird. Full abstraction for functional languages with control. In LICS, 1997. |
| [20] | }}J. Laird. A fully abstract trace semantics for general references. In ICALP, 2007. |
| [21] | }}S. B. Lassen and P. B. Levy. Typed normal form bisimulation. In CSL, 2007. |
| [22] | }}S. B. Lassen and P. B. Levy. Typed normal form bisimulation for parametric polymorphism. In LICS, 2008. 10.1109/LICS.2008.26 |
| [23] | }}I. Mason and C. Talcott. Equivalence in functional languages with effects. JFP, 1(3):287-327, 1991. · Zbl 0941.68540 |
| [24] | }}A. S. Murawski. Functions with local state: regularity and undecidability. TCS, 338(1-3):315-349, 2005. 10.1016/j.tcs.2004.12.036 · Zbl 1108.68076 |
| [25] | }}A. S. Murawski and I. Walukiewicz. Third-order Idealized Algol with iteration is decidable. TCS, 390(2-3):214-229, 2008. 10.1016/j.tcs.2007.09.022 · Zbl 1134.68017 |
| [26] | }}P. O’Hearn and U. Reddy. Objects, interference, and the Yoneda embedding. In MFPS, 1995. |
| [27] | }}A. Pilkiewicz and F. Pottier. The essence of monotonic state. Submitted for publication, 2009. |
| [28] | }}A. Pitts and I. Stark. Operational reasoning for functions with local state. In HOOTS, 1998. |
| [29] | }}A. M. Pitts. Reasoning about local variables with operationally-based logical relations. In LICS, 1996. |
| [30] | }}F. Pottier. Hiding local state in direct style: a higher-order anti-frame rule. In LICS, 2008. 10.1109/LICS.2008.16 |
| [31] | }}F. Pottier. Generalizing the higher-order frame and anti-frame rules. Unpublished, 2009. |
| [32] | }}D. Sangiorgi, N. Kobayashi, and E. Sumii. Environmental bisimulations for higher-order languages. In LICS, 2007. 10.1109/LICS.2007.17 |
| [33] | }}J. Schwinghammer, H. Yang, L. Birkedal, F. Pottier, and B. Reus. A semantic foundation for hidden state. In FOSSACS, 2010. 10.1007/978-3-642-12032-9_2 |
| [34] | }}K. Støvring and S. B. Lassen. A complete, co-inductive syntactic theory of sequential control and state. In POPL, 2007. 10.1145/1190216.1190244 · Zbl 1295.68093 |
| [35] | }}E. Sumii. A complete characterization of observational equivalence in polymorphic λ-calculus with general references. In CSL, 2009. |
| [36] | }}E. Sumii and B. Pierce. A bisimulation for type abstraction and recursion. Journal of the ACM, 54(5):1-43, 2007. 10.1145/1284320.1284325 · Zbl 1326.68073 |
| [37] | }}H. Thielecke. On exceptions versus continuations in the presence of state. In ESOP, 2000. |
| [38] | }}N. Yoshida, K. Honda, and M. Berger. Logical reasoning for higher-order functions with local state. LMCS, 4(4:2), 2008. · Zbl 1161.68031 |
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.
