Aarhus University Seal / Aarhus Universitets segl

Step-indexed relational reasoning for countable nondeterminism

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

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.
Original languageEnglish
Title of host publicationComputer Science Logic (CSL'11) : 25th International Workshop/20th Annual Conference of the EACSL
EditorsMarc Bezem
Number of pages13
PublisherSchloss Dagstuhl--Leibniz-Zentrum für Informatik
Publication year1 Dec 2011
Pages512-524
ISBN (print)9783939897323
DOIs
Publication statusPublished - 1 Dec 2011
Externally publishedYes
SeriesLeibniz International Proceedings in Informatics
Volume12
ISSN1868-8969

    Research areas

  • Countable choice, Lambda calculus, Program equivalence

See relations at Aarhus University Citationformats

ID: 81388125