A Correct Abstract Machine for Safe Ambients

International audienceWe describe an abstract machine, called GcPan, for the dis- tributed execution of Safe Ambients (SA), a variant of the Ambient Calculus (AC).Our machine improves over previous proposals for executing AC, or variants of it, mainly through a better management of special agents (forwarders), created upon code migration to transmit messages to the target location of the migration.We establish the correctness of our machine by proving a weak bisimilarity result with a previous abstract machine for SA, and then appealing to the correctness of the latter machine.More broadly, this study is a contribution towards understanding issues of correctness and optimisations in implementations of distributed languages encompassing mobility