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

Standard

Step-Indexed Relational Reasoning for Countable Nondeterminism. / Birkedal, Lars; Bizjak, Aleš; Schwinghamme, Jan .

In: Logical Methods in Computer Science, Vol. 9, No. 4, 4, 2013.

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

Harvard

Birkedal, L, Bizjak, A & Schwinghamme, J 2013, 'Step-Indexed Relational Reasoning for Countable Nondeterminism', Logical Methods in Computer Science, vol. 9, no. 4, 4. https://doi.org/10.2168/LMCS-9(4:4)2013

APA

Birkedal, L., Bizjak, A., & Schwinghamme, J. (2013). Step-Indexed Relational Reasoning for Countable Nondeterminism. Logical Methods in Computer Science, 9(4), [4]. https://doi.org/10.2168/LMCS-9(4:4)2013

CBE

Birkedal L, Bizjak A, Schwinghamme J. 2013. Step-Indexed Relational Reasoning for Countable Nondeterminism. Logical Methods in Computer Science. 9(4):Article 4. https://doi.org/10.2168/LMCS-9(4:4)2013

MLA

Birkedal, Lars, Aleš Bizjak and Jan Schwinghamme. "Step-Indexed Relational Reasoning for Countable Nondeterminism". Logical Methods in Computer Science. 2013. 9(4). https://doi.org/10.2168/LMCS-9(4:4)2013

Vancouver

Birkedal L, Bizjak A, Schwinghamme J. Step-Indexed Relational Reasoning for Countable Nondeterminism. Logical Methods in Computer Science. 2013;9(4). 4. https://doi.org/10.2168/LMCS-9(4:4)2013

Author

Birkedal, Lars ; Bizjak, Aleš ; Schwinghamme, Jan . / Step-Indexed Relational Reasoning for Countable Nondeterminism. In: Logical Methods in Computer Science. 2013 ; Vol. 9, No. 4.

Bibtex

@article{0fb7f5f0945343078b4b90fdd7a0180a,
title = "Step-Indexed Relational Reasoning for Countable Nondeterminism",
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 ω. ",
author = "Lars Birkedal and Ale{\v s} Bizjak and Jan Schwinghamme",
year = "2013",
doi = "10.2168/LMCS-9(4:4)2013",
language = "English",
volume = "9",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "International Federation for Computational Logic",
number = "4",

}

RIS

TY - JOUR

T1 - Step-Indexed Relational Reasoning for Countable Nondeterminism

AU - Birkedal, Lars

AU - Bizjak, Aleš

AU - Schwinghamme, Jan

PY - 2013

Y1 - 2013

N2 - 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 ω.

AB - 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 ω.

U2 - 10.2168/LMCS-9(4:4)2013

DO - 10.2168/LMCS-9(4:4)2013

M3 - Journal article

VL - 9

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 4

M1 - 4

ER -