Isaac Newton Institute for Mathematical Sciences

Semantics of Computation

1 July - 31 December 1995

Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)

Semantics of Computation Seminar

Wednesday 13 December, 11am

Abstract machines for dialogue games

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.

Copyright © Isaac Newton Institute