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.TYPES.2014.89
URN: urn:nbn:de:0030-drops-54937
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5493/
Go to the corresponding LIPIcs Volume Portal

Hedges, Jules

Dialectica Categories and Games with Bidding

pdf-format:
7.pdf (0.5 MB)

Abstract

This paper presents a construction which transforms categorical models of additive-free propositional linear logic, closely based on de Paiva's dialectica categories and Oliva's functional interpretations of classical linear logic. The construction is defined using dependent type theory, which proves to be a useful tool for reasoning about dialectica categories. Abstractly, we have a closure operator on the class of models: it preserves soundness and completeness and has a monad-like structure. When applied to categories of games we obtain 'games with bidding', which are hybrids of dialectica and game models, and we prove completeness theorems for two specific such models.

BibTeX - Entry

@InProceedings{hedges:LIPIcs:2015:5493,
  author =	{Jules Hedges},
  title =	{{Dialectica Categories and Games with Bidding}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{89--110},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5493},
  URN =		{urn:nbn:de:0030-drops-54937},
  doi =		{10.4230/LIPIcs.TYPES.2014.89},
  annote =	{Keywords: Linear logic, Dialectica categories, categorical semantics, model theory, game semantics, dependent types, functional interpretations}
}

Keywords: Linear logic, Dialectica categories, categorical semantics, model theory, game semantics, dependent types, functional interpretations
Collection: 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Issue Date: 2015
Date of publication: 12.10.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI