00:00:00 / 00:00:00

Program semantics with token passing

By Koko Muroya

Appears in collection : Linear Logic Winter School / École d'hiver de logique linéaire

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 https://dx.doi.org/10.24350/CIRM.V.19883403

Bibliography

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow




Register

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