A type-sound calculus of computational fields

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. 

keywords   Computational field

journal or series

 Science of Computer Programming (SCP)

funding project

 CINA — Compositionality, Interaction, Negotiation, Autonomicity for the future ICT society (01/01/2013–31/12/2015)