A higher-order functional language supports a higher-order store (or general storage) just if
Historically, the first language with a higher-order store was CPL. However, it was an advanced feature of CPL, and appears to never have been implemented.
Today, the most common languages with a higher-order store are
The presence of a higher-order store means that recursion is possible, as it can be encoded using function storage.
The trick for doing so is known as Landin's knot.
It is devilishly difficult to produce semantic models of higher-order store.
These difficulties started becoming apparent very early on, even in the early 1970s: see [Tennent and Ghica 2000]. A paper by Christopher Strachey entitled An abstract model of storage was supposed to appear after 1972, but never materialised.
The Revised Reports on Scheme describe some kind of model of higher-order store using the solution to domain-theoretic equations. It is not known whether this is mathematically well-behaved, but the implication is that it is not.
In the last section of the 1996 survey of open problems in domain-theoretic modelling of programming languages [Jung et al 1996], Ian Stark surveys the state of the art in domain-theoretic modelling at the time.
The first fully abstract model of general references was presented at LICS 1998 [Abramsky, Honda, McCusker 1998]. It is based on game semantics.
A possible worlds model of higher-order storage in a call-by-value setting was presented by Paul Blain Levy at CSL 2002 [Levy 2002]. Some discussion of this may also be found in the 2003 call-by-push-value book.
More recent models of general storage use a combination of possible worlds and realizability, in particular step-indexing. These models side-step the solution of difficult domain equations in parametric settings. Though very syntactic, these types of models have proven surprisingly effective at proving type safety, validating program logics, and reasoning about complicated languages that combine all these features.
Tennent, Robert D., and Dan R. Ghica. 2000. ‘Abstract Models of Storage’. Higher-Order and Symbolic Computation 13: 119–29. https://doi.org/10.1023/A:1010022312623. [pdf]
@article{tennent_2000,
title = {Abstract {Models} of {Storage}},
volume = {13},
doi = {10.1023/A:1010022312623},
journal = {Higher-Order and Symbolic Computation},
author = {Tennent, Robert D. and Ghica, Dan R.},
year = {2000},
pages = {119--129}
}
Fiore, M. P., A. Jung, E. Moggi, P. O’Hearn, J. Riecke, G. Rosolini, and I. Stark. 1996. ‘Domains and Denotational Semantics: History, Accomplishments and Open Problems’. Bulletin of the European Association for Theoretical Computer Science 59: 227–56. [pdf]
@article{jung_1996,
title = {Domains and {Denotational} {Semantics}: {History}, {Accomplishments} and {Open} {Problems}},
volume = {59},
journal = {Bulletin of the European Association for Theoretical Computer Science},
author = {Jung, A. and Fiore, M. P. and Moggi, E. and O'Hearn, P. and Riecke, J. and Rosolini, G. and Stark, I.},
year = {1996},
pages = {227--256}
}
Abramsky, Samson, Kohei Honda, and G McCusker. 1998. ‘A Fully Abstract Game Semantics for General References’. In Proceedings of TheThirteenth Annual IEEE Symposium on Logic in Computer Science. IEEE. https://doi.org/10.1109/LICS.1998.705669.
@inproceedings{abramsky_fully_1998,
title = {A fully abstract game semantics for general references},
doi = {10.1109/LICS.1998.705669},
booktitle = {Proceedings of {theThirteenth} {Annual} {IEEE} {Symposium} on {Logic} in {Computer} {Science}},
publisher = {IEEE},
author = {Abramsky, Samson and Honda, Kohei and McCusker, G},
year = {1998}
}
Levy, Paul Blain. 2002. ‘Possible World Semantics for General Storage in Call-By-Value’. In Computer Science Logic, edited by Julian Bradfield, 2471:232–46. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-45793-3_16.
@inproceedings{levy_2002,
address = {Berlin, Heidelberg},
title = {Possible {World} {Semantics} for {General} {Storage} in {Call}-{By}-{Value}},
volume = {2471},
doi = {10.1007/3-540-45793-3_16},
booktitle = {Computer {Science} {Logic}},
publisher = {Springer Berlin Heidelberg},
author = {Levy, Paul Blain},
editor = {Bradfield, Julian},
year = {2002},
pages = {232--246}
}