Krivine Nets

Add to your list(s) Download to your calendar using vCal

• Olle Fredriksson (University of Birmingham)
• Monday 05 May 2014, 13:00-14:00
• CS 217.

If you have a question about this talk, please contact Neel Krishnaswami.

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.

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 217
• Lab Lunch

Note that ex-directory lists are not shown.