The Parallel Intensionally Fully Abstract Games Model of PCF
Autor: | Pierre Clairambault, Simon Castellan, Glynn Winskel |
---|---|
Přispěvatelé: | Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Preuves et Langages (PLUME), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Computer Laboratory [Cambridge], University of Cambridge [UK] (CAM), ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), Université de Lyon-École normale supérieure - Lyon (ENS Lyon)-Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL) |
Jazyk: | angličtina |
Rok vydání: | 2015 |
Předmět: |
Theoretical computer science
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Game semantics Computer science Programming language Event (computing) Semantics (computer science) [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 16. Peace & justice computer.software_genre Plot (graphics) Interpretation (model theory) TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Concurrent computing computer |
Zdroj: | Thirtieth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) Thirtieth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2015, Kyoto, Japan. ⟨10.1109/LICS.2015.31⟩ LICS |
DOI: | 10.1109/LICS.2015.31⟩ |
Popis: | International audience; We describe a framework for truly concurrent game semantics of programming languages, based on Rideau and Winskel's concurrent games on event structures. The model supports a notion of innocent strategy that permits concurrent and non-deterministic behaviour, but which coincides with traditional Hyland-Ong innocent strategies if one restricts to the deterministic sequential case. In this framework we give an alternative interpretation of Plotkin's PCF, that takes advantage of the concurrent nature of strategies and formalizes the idea that although PCF is a sequential language, certain sub-computations are independent and can be computed in a parallel fashion. We show that just as Hyland and Ong's sequential interpretation of PCF, our parallel interpretation yields a model that is intensionally fully abstract for PCF. |
Databáze: | OpenAIRE |
Externí odkaz: |