The Machinery of Interaction

Abstract: Girard's geometry of interaction suggests an unusual way of evaluating lambda terms, the interaction abstract machine (IAM), first studied by Mackie and Danos & Regnier in the nineties, using linear logic proof nets. In particular, the IAM does not use environments, in contrast to the mainstream approach to abstract machines. In this talk I shall give a slow paced introduction to the IAM, using an alternative presentation based on ordinary lambda terms. If time permits, I shall also discuss how to measure the time and space consumptions of the IAM via multi types. This talk is an overview of joint works with Ugo Dal Lago and Gabriele Vanoni.

logic in computer scienceprogramming languages

Audience: researchers in the topic

LoReL Seminar

Series comments: Talks are either in Spanish or English, however they can often be in English upon request.