article · 2008

Extensional semantics of program behaviour

Guy McCusker

Cited by 0Abstract and details only

Abstract

Game semantics is a way of characterizing programming languages and logical calculi intensionally by interpreting proofs or programs as strategies for interacting with the environment; this process of interaction can be thought of as playing a two-person game. Games can capture precisely the behaviour of higher-order programs in sequential languages, in a fashion which is very difficult or impossible for traditional forms of denotational semantics. This precision can be expressed formally via the properties of full abstraction, full completeness or universality. A remarkable feature of game semantics is its flexibility: games have been used to give fully abstract or fully complete models not only of logics such as linear logic [3] and functional languages such as PCF [1, 12, 38], but also languages with powerful imperative features such as references (state) [4, 2], continuations [32] and exceptions [13]. By contrast, in domain theory programs are modelled extensionally using sets (with certain order-theoretic structure) and functions (preserving that structure). Domains have formed the basis for much research in denotational semantics by virtue of their conceptual simplicity, and now form a wide-ranging mathematical theory. The search for order-theoretic characterizations of higher-order sequentiality has led to the development of several candidate notions, such as stability [5] and strong stability [6], and was arguably the driving force behind most work in denotational semantics for some years. However, a significant obstacle to the use of domains to reason about programming languages has been a lack of accurate models of imperative and concurrent features of the sort provided by game semantics. A possible basis for connecting the intensional world of games with the extensional world of domains was the remarkable observation of Cartwright and Felleisen [8]\n\n

Cite this paper

APA 7

McCusker, G. (2008). Extensional semantics of program behaviour.

MLA 9

McCusker, Guy. “Extensional semantics of program behaviour.” 2008.

Chicago

McCusker, Guy. 2008. “Extensional semantics of program behaviour.”

Harvard

McCusker, G. (2008) ‘Extensional semantics of program behaviour’.

BibTeX

@article{mccusker2008extensional,
  title = {{Extensional semantics of program behaviour}},
  author = {McCusker, Guy},
  year = {2008}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.