We study the semantic meaning of block structure using game semantics and introduce the notion of block-innocent strategies, which turns out to characterise call-by-value computation with block-allocated storage through soundness, finitary definability and universality results. This puts us in a good position to conduct a comparative study of purely functional computation, computation with block storage and dynamic memory allocation respectively. For example, we show that dynamic variable allocation can be replaced with block-allocated variables exactly when the term involved (open or closed) is of base type and that block-allocated storage can be replaced with purely functional computation when types of order two are involved. To illustrate the restrictive nature of block structure further, we prove a decidability result for a finitary fragment of call-by-value Idealized Algol for which it is known that allowing for dynamic memory allocation leads to undecidability. © 2010 Springer-Verlag.
CITATION STYLE
Murawski, A. S., & Tzevelekos, N. (2010). Block structure vs. scope extrusion: Between innocence and omniscience. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6014 LNCS, pp. 33–47). https://doi.org/10.1007/978-3-642-12032-9_4
Mendeley helps you to discover research relevant for your work.