some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

   Volume 2 (2006)

   Volume 3 (2007)

   Volume 4 (2008)

   Volume 5 (2009)

   Volume 6 (2010)

   Volume 7 (2011)

   Volume 8 (2012)

   Volume 9 (2013)

      Issue 1

      Issue 2

      Issue 3

      Issue 4

   Volume 10 (2014)

   Volume 11 (2015)

   Volume 12 (2016)

   Volume 13 (2017)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

VOLUME 9, ISSUE 4, PAPER 4


Step-Indexed Relational Reasoning for Countable Nondeterminism

©Lars Birkedal, IT University of Copenhagen
©Aleš Bizjak, Aarhus University, Denmark
©Jan Schwinghammer, Saarland University

Abstract
Programming languages with countable nondeterministic choice are computationally interesting since countable nondeterminism arises when modeling fairness for concurrent systems. Because countable choice introduces non-continuous behaviour, it is well-known that developing semantic models for programming languages with countable nondeterminism is challenging. We present a step-indexed logical relations model of a higher-order functional programming language with countable nondeterminism and demonstrate how it can be used to reason about contextually defined may- and must-equivalence. In earlier step-indexed models, the indices have been drawn from ω. Here the step-indexed relations for must-equivalence are indexed over an ordinal greater than ω.

Publication date: October 15, 2013

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-9(4:4)2013

Hit Counts: 3992

Creative Commons