Block structure vs scope extrusion: between innocence and omniscience

DOI10.2168/LMCS-12(3:3)2016MaRDI QIDQ2974774zbMATH OpenFDO

Authors Andrzej S. Murawski, Nikos Tzevelekos

Publication date 11 April 2017

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1605.02311

zbMATH Keywords

contextual equivalencegame semanticsreferences

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Abstract: 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.

Recommendations

• Block structure vs. scope extrusion: between innocence and omniscience
• scientific article; zbMATH DE number 3970088
• Polymorphic game semantics for dynamic binding
• scientific article; zbMATH DE number 3949678
• scientific article; zbMATH DE number 1231510

Cites work

• A fragment of ML decidable by visibly pushdown automata
• A new approach to abstract syntax with variable binding
• About the undecidability of program equivalence in finitary languages with state
• Automata, Languages and Programming
• Block structure vs. scope extrusion: between innocence and omniscience
• Fragments of ML decidable by nested data class memory automata
• Full abstraction for idealized Algol with passive expressions
• Full abstraction for nominal general references
• Full abstraction for PCF
• Functions with local state: regularity and undecidability
• Game-theoretic analysis of call-by-value computation
• scientific article; zbMATH DE number 3949678 (Why is no real title available?)
• scientific article; zbMATH DE number 1223609 (Why is no real title available?)
• scientific article; zbMATH DE number 1231510 (Why is no real title available?)
• LCF considered as a programming language
• On full abstraction for PCF: I, II and III
• Regular-language semantics for a call-by-value programming language
• Semantics for local computational effects

Cited in

(3)

• On block structures in quantum computation
• Block structure vs. scope extrusion: between innocence and omniscience
• A fully abstract game semantics for countable nondeterminism

Describes a project that uses

Uses Software

• ML

This page was built for publication: Block structure vs scope extrusion: between innocence and omniscience

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2974774)