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

lmcs:2007 - Logical Methods in Computer Science, August 17, 2016, Volume 12, Issue 3
Block structure vs scope extrusion: between innocence and omniscience

Authors: Murawski, Andrzej S. and Tzevelekos, Nikos

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.


Source : oai:arXiv.org:1605.02311
DOI : 10.2168/LMCS-12(3:3)2016
Volume: Volume 12, Issue 3
Published on: August 17, 2016
Submitted on: August 17, 2016
Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,D.3.1


Share

Browsing statistics

This page has been seen 101 times.
This article's PDF has been downloaded 33 times.