Aarhus University Seal / Aarhus Universitets segl

Step-Indexed Relational Reasoning for Countable Nondeterminism

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

  • Lars Birkedal
  • Aleš Bizjak, Denmark
  • Jan Schwinghamme, aarland University, Germany
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 ω.
Original languageEnglish
Article number4
JournalLogical Methods in Computer Science
Number of pages22
Publication statusPublished - 2013

See relations at Aarhus University Citationformats

ID: 68518886