Linear Logic Winter School / École d'hiver de logique linéaire

Collection Linear Logic Winter School / École d'hiver de logique linéaire

Organizer(s) Tortora de Falco, Lorenzo ; Vaux Auclair, Lionel
Date(s) 1/24/22 - 1/28/22
linked URL
00:00:00 / 00:00:00
5 6

Program semantics with token passing

By Koko Muroya

Geometry of Interaction, combined with translation of lambda-calculus into MELL proof nets, has enabled an unconventional approach to program semantics. Danos and Regnier, and Mackie pioneered the approach, and introduced the so-called token-passing machines. It turned out that the unconventional token-passing machines can be turned into a graphical realisation of conventional reduction semantics, in a simple way. The resulting semantics can be more convenient than the standard (syntactical) reduction semantics, in analysing local behaviour of programs. I will explain how, in particular, the resulting graphical reduction semantics can be used to reason about observational equivalence between programs.

Information about the video

Citation data


Last related questions on MathOverflow

You have to connect your account with mathoverflow to add question

Ask a question on MathOverflow


  • Bookmark videos
  • Add videos to see later &
    keep your browsing history
  • Comment with the scientific
  • Get notification updates
    for your favorite subjects
Give feedback