Lars Birkedal ; Aleš Bizjak ; Jan Schwinghammer - Step-Indexed Relational Reasoning for Countable Nondeterminism

lmcs:940 - Logical Methods in Computer Science, October 15, 2013, Volume 9, Issue 4 - https://doi.org/10.2168/LMCS-9(4:4)2013
Step-Indexed Relational Reasoning for Countable Nondeterminism

Authors: Lars Birkedal ; Aleš Bizjak ; Jan Schwinghammer

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 {\omega}. Here the step-indexed relations for must-equivalence are indexed over an ordinal greater than {\omega}.


Volume: Volume 9, Issue 4
Published on: October 15, 2013
Accepted on: June 25, 2015
Submitted on: March 6, 2012
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 507 times.
This article's PDF has been downloaded 172 times.