Block structure vs. scope extrusion: Between innocence and omniscience

4Citations
Citations of this article
6Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free