2026-07-20T15:08:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3253 2024-03-06T10:34:01Z ddc:004 open_access

Step-Indexed Relational Reasoning for Countable Nondeterminism Schwinghammer, Jan Birkedal, Lars countable choice lambda calculus program equivalence 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jan Schwinghammer and Lars Birkedal 2011 Is Part Of LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2011.512 urn:nbn:de:0030-drops-32535 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.512 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode