Français
Program semantics with token passing
Virtualconference
Authors : Muroya, Koko (Author of the conference)
CIRM (Publisher )
68-01 - Instructional exposition (textbooks, tutorial papers, etc.)
68N18 - Functional programming and lambda calculus
68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Additional resources :
https://www.cirm-math.fr/RepOrga/2685/Slides/2022-01-28-1-muroya.pdf
CIRM (Publisher )
Loading the player...
|
Abstract :
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.
Keywords : Geometry of interaction; lambda-calculus; abstract machine
MSC Codes : 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.
Keywords : Geometry of interaction; lambda-calculus; abstract machine
68-01 - Instructional exposition (textbooks, tutorial papers, etc.)
68N18 - Functional programming and lambda calculus
68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Additional resources :
https://www.cirm-math.fr/RepOrga/2685/Slides/2022-01-28-1-muroya.pdf
|
Information on the Video
Film maker : Hennenfent, GuillaumeLanguage : English Available date : 14/02/2022 Conference Date : 28/01/2022 Subseries : Research School arXiv category : Logic in Computer Science ; Programming Languages Mathematical Area(s) : Computer Science Format : MP4 (.mp4) - HD Video Time : 00:28:47 Targeted Audience : Researchers ; Graduate Students ; Doctoral Students, Post-Doctoral Students Download : https://videos.cirm-math.fr/2022-01-28_Muroya.mp4 
|
Information on the Event
Event Title : Linear Logic Winter School / École d'hiver de logique linéaireEvent Organizers : Tortora de Falco, Lorenzo ; Vaux Auclair, Lionel Dates : 24/01/2022 - 28/01/2022 Event Year : 2022 Event URL : https://conferences.cirm-math.fr/2685.html
Citation Data
DOI : 10.24350/CIRM.V.19883403Cite this video as: Muroya, Koko (2022). Program semantics with token passing. CIRM. Audiovisual resource. doi:10.24350/CIRM.V.19883403 URI : http://dx.doi.org/10.24350/CIRM.V.19883403 |
See Also
- [Multi angle] Focused proof systems / Author of the conference Miller, Dale.
- [Multi angle] Heterodox exponential modalities in linear logic / Author of the conference Mazza, Damiano.
- [Multi angle] Taylor expansion, at work / Author of the conference Manzonetto, Giulio.
- [Multi angle] Differential linear logic extended to differential operators / Author of the conference Kerjean, Marie.
- [Multi angle] Deux ou trois choses que je sais d'elle : la logique / Author of the conference Girard, Jean-Yves.
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
Imagette Video
