English
Program semantics with token passing
Virtualconference
Auteurs : Muroya, Koko (Auteur de la Conférence)
CIRM (Editeur )
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.)
Ressources complémentaires :
https://www.cirm-math.fr/RepOrga/2685/Slides/2022-01-28-1-muroya.pdf
CIRM (Editeur )
Loading the player...
|
Résumé :
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
Codes MSC : 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.)
Ressources complémentaires :
https://www.cirm-math.fr/RepOrga/2685/Slides/2022-01-28-1-muroya.pdf
|
Informations sur la Vidéo
Réalisateur : Hennenfent, GuillaumeLangue : Anglais Date de publication : 14/02/2022 Date de captation : 28/01/2022 Sous collection : Research School arXiv category : Logic in Computer Science ; Programming Languages Domaine : Computer Science Format : MP4 (.mp4) - HD Durée : 00:28:47 Audience : Researchers ; Graduate Students ; Doctoral Students, Post-Doctoral Students Download : https://videos.cirm-math.fr/2022-01-28_Muroya.mp4 
|
Informations sur la Rencontre
Nom de la rencontre : Linear Logic Winter School / École d'hiver de logique linéaireOrganisateurs de la rencontre : Tortora de Falco, Lorenzo ; Vaux Auclair, Lionel Dates : 24/01/2022 - 28/01/2022 Année de la rencontre : 2022 URL Congrès : https://conferences.cirm-math.fr/2685.html
Données de citation
DOI : 10.24350/CIRM.V.19883403Citer cette vidéo: 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 |
Voir aussi
- [Multi angle] Focused proof systems / Auteur de la Conférence Miller, Dale.
- [Multi angle] Heterodox exponential modalities in linear logic / Auteur de la Conférence Mazza, Damiano.
- [Multi angle] Taylor expansion, at work / Auteur de la Conférence Manzonetto, Giulio.
- [Multi angle] Differential linear logic extended to differential operators / Auteur de la Conférence Kerjean, Marie.
- [Multi angle] Deux ou trois choses que je sais d'elle : la logique / Auteur de la Conférence Girard, Jean-Yves.
Bibliographie
- 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
