A type-sound calculus of computational fields

   page       BibTeX_logo.png       attach   
Ferruccio Damiani, Mirko Viroli, Jacob Beal
Science of Computer Programming 117, pages 17–44
2016

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.

keywordsComputational field, Core calculus, Operational semantics, Spatial computing, Type soundness
journal or series
book Science of Computer Programming (SCP)
funding project
wrenchCINA — Compositionality, Interaction, Negotiation, Autonomicity for the future ICT society (01/01/2013–31/12/2015)