1 July - 31 December 1995
Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)
Wednesday 13 December, 11am
Pierre-Louis Curien (Paris ENS and Newton Inst.)
We present a general, type-free computing device, tentatively called the Strategic Abstract Machine (SAM), applying to lambda-calculus, to PCF, to cut-elimination, say, in Novikoff's logic (following Thierry Coquand), and more generally to trees with pointers (witnessing bindings). We present two other mechanisms: the Coquand-Herbelin-Hyland-Ong mechanism based on views, and one which arises from Danos and Regnier's understanding of Krivine's machine. All these mechanisms are equivalent, i.e. define the same cut-elimination (or composition) functions.