AnImperativePureCalculus.pdf (259.18 kB)

An Imperative Pure Calculus

Download (259.18 kB)
conference contribution
posted on 01.11.2020, 23:01 by A Capriccioli, Marco Servetto, E Zucca
© 2016 The Authors. Published by Elsevier B.V. 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.

History

Preferred citation

Capriccioli, A., Servetto, M. & Zucca, E. (2016, April). An Imperative Pure Calculus. In Electronic Notes in Theoretical Computer Science (322 (2016)pp. 87-102). Elsevier. https://doi.org/10.1016/j.entcs.2016.03.007

Title of proceedings

Electronic Notes in Theoretical Computer Science

Volume

322

Series

Electronic Notes in Theoretical Computer Science

Contribution type

Published Paper

Publication or Presentation Year

18/04/2016

Pagination

87-102

Publisher

Elsevier

Publication status

Published

ISSN

1571-0661

Licence

Exports