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 - https://doi.org/10.2168/LMCS-12(3:3)2016
Block structure vs scope extrusion: between innocence and omniscienceArticle

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
    Accepted on: August 17, 2016
    Submitted on: October 31, 2015
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,D.3.1
    Funding:
      Source : OpenAIRE Graph
    • Logic of Interaction and Information Flow; Funder: UK Research and Innovation; Code: EP/F067607/1

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1843 times.
    This article's PDF has been downloaded 463 times.