Abstract machines for game semantics, revisited

Research output: Contribution to journalConference articlepeer-review

Standard

Abstract machines for game semantics, revisited. / Fredriksson, Olle; Ghica, Dan R.

In: Proceedings - Symposium on Logic in Computer Science, 09.09.2013, p. 560-569.

Research output: Contribution to journalConference articlepeer-review

Harvard

APA

Vancouver

Author

Bibtex

@article{aae6631bbd7549cc941311ea1fc653d8,
title = "Abstract machines for game semantics, revisited",
abstract = "We define new abstract machines for game semantics which correspond to networks of conventional computers, and can be used as an intermediate representation for compilation targeting distributed systems. This is achieved in two steps. First we introduce the HRAM, a Heap and Register Abstract Machine, an abstraction of a conventional computer, which can be structured into HRAM nets, an abstract point-to-point network model. HRAMs are multi-threaded and subsume communication by tokens (cf. IAM) or jumps. Game Abstract Machines (GAM), are HRAMs with additional structure at the interface level, but no special operational capabilities. We show that GAMs cannot be naively composed, but composition must be mediated using appropriate HRAM combinators. HRAMs are flexible enough to allow the representation of game models for languages with state (non-innocent games) or concurrency (non-Alternating games). We illustrate the potential of this technique by implementing a toy distributed compiler for ICA, a higher-order programming language with shared state concurrency, thus significantly extending our previous distributed PCF compiler. We show that compilation is sound and memory-safe, i.e. no (distributed or local) garbage collection is necessary.",
keywords = "abstract machines, distributed compilation, game semantics",
author = "Olle Fredriksson and Ghica, {Dan R.}",
year = "2013",
month = sep,
day = "9",
doi = "10.1109/LICS.2013.63",
language = "English",
pages = "560--569",
journal = "Proceedings - Symposium on Logic in Computer Science",
issn = "1043-6871",
publisher = "Institute of Electrical and Electronics Engineers (IEEE)",
note = "2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013 ; Conference date: 25-06-2013 Through 28-06-2013",

}

RIS

TY - JOUR

T1 - Abstract machines for game semantics, revisited

AU - Fredriksson, Olle

AU - Ghica, Dan R.

PY - 2013/9/9

Y1 - 2013/9/9

N2 - We define new abstract machines for game semantics which correspond to networks of conventional computers, and can be used as an intermediate representation for compilation targeting distributed systems. This is achieved in two steps. First we introduce the HRAM, a Heap and Register Abstract Machine, an abstraction of a conventional computer, which can be structured into HRAM nets, an abstract point-to-point network model. HRAMs are multi-threaded and subsume communication by tokens (cf. IAM) or jumps. Game Abstract Machines (GAM), are HRAMs with additional structure at the interface level, but no special operational capabilities. We show that GAMs cannot be naively composed, but composition must be mediated using appropriate HRAM combinators. HRAMs are flexible enough to allow the representation of game models for languages with state (non-innocent games) or concurrency (non-Alternating games). We illustrate the potential of this technique by implementing a toy distributed compiler for ICA, a higher-order programming language with shared state concurrency, thus significantly extending our previous distributed PCF compiler. We show that compilation is sound and memory-safe, i.e. no (distributed or local) garbage collection is necessary.

AB - We define new abstract machines for game semantics which correspond to networks of conventional computers, and can be used as an intermediate representation for compilation targeting distributed systems. This is achieved in two steps. First we introduce the HRAM, a Heap and Register Abstract Machine, an abstraction of a conventional computer, which can be structured into HRAM nets, an abstract point-to-point network model. HRAMs are multi-threaded and subsume communication by tokens (cf. IAM) or jumps. Game Abstract Machines (GAM), are HRAMs with additional structure at the interface level, but no special operational capabilities. We show that GAMs cannot be naively composed, but composition must be mediated using appropriate HRAM combinators. HRAMs are flexible enough to allow the representation of game models for languages with state (non-innocent games) or concurrency (non-Alternating games). We illustrate the potential of this technique by implementing a toy distributed compiler for ICA, a higher-order programming language with shared state concurrency, thus significantly extending our previous distributed PCF compiler. We show that compilation is sound and memory-safe, i.e. no (distributed or local) garbage collection is necessary.

KW - abstract machines

KW - distributed compilation

KW - game semantics

UR - http://www.scopus.com/inward/record.url?scp=84883399870&partnerID=8YFLogxK

U2 - 10.1109/LICS.2013.63

DO - 10.1109/LICS.2013.63

M3 - Conference article

AN - SCOPUS:84883399870

SP - 560

EP - 569

JO - Proceedings - Symposium on Logic in Computer Science

JF - Proceedings - Symposium on Logic in Computer Science

SN - 1043-6871

M1 - 6571589

T2 - 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013

Y2 - 25 June 2013 through 28 June 2013

ER -