Title
An Imperative Pure Calculus.
Abstract
We present a simple calculus where imperative features are modeled by just rewriting source code terms, rather than by modifying an auxiliary structure which mimics physical memory. Formally, this is achieved by the block construct, introducing local variable declarations, which also plays the role of store when such declarations have been evaluated. In this way, we obtain a language semantics which is more abstract, and directly represents at the syntactic level constraints on aliasing, allowing simpler reasoning about related properties. We illustrate this possibility by a simple extension of the standard type system which assigns a capsule tag to expressions that will reduce to (values representing) isolated portions of store.
Year
DOI
Venue
2016
10.1016/j.entcs.2016.03.007
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
operational semantics,imperative calculus,aliasing
Simple extension,Operational semantics,Programming language,Expression (mathematics),Computer science,Source code,Theoretical computer science,Aliasing,Rewriting,Syntax,Local variable,Calculus
Journal
Volume
Issue
ISSN
322
C
1571-0661
Citations 
PageRank 
References 
4
0.43
12
Authors
3
Name
Order
Citations
PageRank
Andrea Capriccioli140.43
Marco Servetto26111.51
Elena Zucca3497101.25