Portal de Periódicos da CAPES

An Abstract Machine for the Kell Calculus

2005; Springer Science+Business Media; Linguagem: Inglês

10.1007/11494881_3

1611-3349

Philippe Bidinger, Alan Schmitt, Jean‐Bernard Stefani,

Logic, programming, and type systems

The Kell Calculus is a family of process calculi intended as a basis for studying distributed component-based programming. This paper presents an abstract machine for an instance of this calculus, a proof of its correctness, and a prototype OCaml implementation. The main originality of our abstract machine is that it does not mandate a particular physical configuration (e.g. mapping of localities to physical sites), and it is independent of any supporting network services. This allows to separate the proof of correctness of the abstract machine per se, from the proof of correctness of higher-level communication and migration protocols which can be implemented on the machine.