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 https://conferences.cirm-math.fr/2685.html

00:00:00 / 00:00:00

5 6

Program semantics with token passing

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

Date of recording 1/28/22
Date of publication 2/14/22
Institution CIRM
Licence CC BY NC ND
Language English
Audience Researchers, Graduate Students
Director(s) Guillaume Hennenfent
Format MP4

Citation data

DOI 10.24350/CIRM.V.19883403
Cite this video Muroya Koko (1/28/22). Program semantics with token passing. CIRM. Audiovisual resource. DOI: 10.24350/CIRM.V.19883403
URL https://dx.doi.org/10.24350/CIRM.V.19883403

Domain(s)

Bibliography

MUROYA, Koko. Hypernet semantics of programming languages. 2020. Thèse de doctorat. University of Birmingham. - http://etheses.bham.ac.uk/id/eprint/10433
GHICA, Dan R. et MUROYA, Koko. The dynamic Geometry of Interaction machine: a token-guided graph rewriter. Logical Methods in Computer Science, 2019, vol. 15. - https://doi.org/10.23638/LMCS-15(4:7)2019
DANOS, Vincent et REGNIER, Laurent. Reversible, irreversible and optimal λ-machines. Electronic Notes in Theoretical Computer Science, 1996, vol. 3, p. 40-60. - https://doi.org/10.1016/S1571-0661(05)80402-5
MACKIE, Ian. The geometry of interaction machine. In : Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 1995. p. 198-208. - https://doi.org/10.1145/199448.199483

MSC codes

Document(s)

https://www.cirm-math.fr/RepOrga/2685/Slides/2022-01-28-1-muroya.pdf

Last related questions on MathOverflow

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

Ask a question on MathOverflow

All the collection videos

01:44:57

published on February 14, 2022

Deux ou trois choses que je sais d'elle : la logique

By Jean-Yves Girard

31:21

published on February 14, 2022

Taylor expansion, at work

By Giulio Manzonetto

34:22

published on February 14, 2022

Heterodox exponential modalities in linear logic

By Damiano Mazza

28:43

published on February 14, 2022

Focused proof systems

By Dale Miller

28:47

published on February 14, 2022

Program semantics with token passing

By Koko Muroya

24:39

published on February 14, 2022

Differential linear logic extended to differential operators

By Marie Kerjean

Copyright Carmin.tv 2023

Give feedback