Abstract
We define a new approach to compilation to distributed architectures based on networks of abstract machines. Using it we can implement a generalised and fully transparent form of Remote Procedure Call that supports calling higher-order functions across node boundaries, without sending actual code. Our starting point is the classic Krivine machine, which implements reduction for untyped call-by-name PCF. We successively add the features that we need for distributed execution and show the correctness of each addition. Then we construct a two-level operational semantics, where the high level is a network of communicating machines, and the low level is given by local machine transitions. Using these networks, we arrive at our final system, the Krivine Net. We show that Krivine Nets give a correct distributed implementation of the Krivine machine, which preserves both termination and non-termination properties. All the technical results have been formalised and proved correct in Agda. We also implement a prototype compiler which we compare with previous distributing compilers based on Girard's Geometry of Interaction and on Game Semantics.
Original language | English |
---|---|
Title of host publication | Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP 2014 |
Publisher | Association for Computing Machinery |
Pages | 349-361 |
Number of pages | 13 |
ISBN (Print) | 9781450328739 |
DOIs | |
Publication status | Published - 1 Sept 2014 |
Event | 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014 - Gothenburg, Sweden Duration: 1 Sept 2014 → 3 Sept 2014 |
Conference
Conference | 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014 |
---|---|
Country/Territory | Sweden |
City | Gothenburg |
Period | 1/09/14 → 3/09/14 |
Keywords
- abstract machines
- agda
- distributed execution
- simulation relation
ASJC Scopus subject areas
- Software