License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2013.231
URN: urn:nbn:de:0030-drops-42005
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4200/
Di Gianantonio, Pietro ;
Lenisa, Marina
Innocent Game Semantics via Intersection Type Assignment Systems
Abstract
The aim of this work is to correlate two different approaches to the semantics of programming languages: game semantics and intersection type assignment systems (ITAS). Namely, we present an ITAS that provides the description of the semantic interpretation of a typed lambda calculus in a game model based on innocent strategies. Compared to the traditional ITAS used to describe the semantic interpretation in domain theoretic models, the ITAS presented in this paper has two main differences: the introduction of a notion of labelling on moves, and the omission of several rules, i.e. the subtyping rules and some structural rules.
BibTeX - Entry
@InProceedings{digianantonio_et_al:LIPIcs:2013:4200,
author = {Pietro Di Gianantonio and Marina Lenisa},
title = {{Innocent Game Semantics via Intersection Type Assignment Systems}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {231--247},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-60-6},
ISSN = {1868-8969},
year = {2013},
volume = {23},
editor = {Simona Ronchi Della Rocca},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/4200},
URN = {urn:nbn:de:0030-drops-42005},
doi = {10.4230/LIPIcs.CSL.2013.231},
annote = {Keywords: Game Semantics, Intersection Type Assignment System, Lambda Calculus}
}
|
Keywords: |
|
Game Semantics, Intersection Type Assignment System, Lambda Calculus |
|
Collection: |
|
Computer Science Logic 2013 (CSL 2013) |
|
Issue Date: |
|
2013 |
|
Date of publication: |
|
02.09.2013 |
