Andrzej S. Murawski ; Nikos Tzevelekos - Block structure vs scope extrusion: between innocence and omniscience

lmcs:2007 - Logical Methods in Computer Science, April 27, 2017, Volume 12, Issue 3 -
Block structure vs scope extrusion: between innocence and omniscience

Authors: Andrzej S. Murawski ; Nikos Tzevelekos

We study the semantic meaning of block structure using game semantics. To that end, we introduce the notion of block-innocent strategies and characterise call-by-value computation with block-allocated storage through soundness, finite definability and universality results. This puts us in a good position to conduct a comparative study of purely functional computation, computation with block storage as well as that with dynamic memory allocation. For example, we can 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.

Volume: Volume 12, Issue 3
Published on: April 27, 2017
Submitted on: October 31, 2015
Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,D.3.1


Consultation statistics

This page has been seen 508 times.
This article's PDF has been downloaded 252 times.