Logo image
Back
A type-sound calculus of computational fields
Journal article   Open access   Peer reviewed

A type-sound calculus of computational fields

Ferruccio Damiani, Mirko Viroli and Jacob Beal
Science of computer programming, Vol.117, pp.17-44
02/15/2016
DOI: 10.1016/j.scico.2015.11.005
url
https://doi.org/10.1016/j.scico.2015.11.005View
Published (Version of record) Open Access

Abstract

A number of recent works have investigated the notion of “computational fields” as a means of coordinating systems in distributed, dense and dynamic environments such as pervasive computing, sensor networks, and robot swarms. We introduce a minimal core calculus meant to capture the key ingredients of languages that make use of computational fields: functional composition of fields, functions over fields, evolution of fields over time, construction of fields of values from neighbours, and restriction of a field computation to a sub-region of the network. We formalise a notion of type soundness for the calculus that encompasses the concept of domain alignment, and present a sound static type inference system. This calculus and its type inference system can act as a core for actual implementation of coordination languages and models, as well as to pave the way towards formal analysis of properties concerning expressiveness, self-stabilisation, topology independence, and relationships with the continuous space–time semantics of spatial computations. •We introduce a core calculus for the notion of computational fields.•We illustrate applications to self-organising spatial structures.•We introduce a type inference system a la ML for the proposed calculus, capturing key requirements on “domain alignment”.•We prove type soundness.
 Computational field Core calculus Operational semantics Spatial computing Type soundness

Details

Metrics

18 Record Views
27 Times Cited - Web of Science
Logo image