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) 24/01/2022 - 28/01/2022
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

  • DOI 10.24350/CIRM.V.19883403
  • Cite this video Muroya, Koko (28/01/2022). Program semantics with token passing. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.19883403
  • URL


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
Loading the web debug toolbar…
Attempt #