Step-Indexed Relational Reasoning for Countable Nondeterminism

Schwinghammer, Jan; Birkedal, Lars

doi:10.4230/LIPIcs.CSL.2011.512

Document

Step-Indexed Relational Reasoning for Countable Nondeterminism

Authors Jan Schwinghammer, Lars Birkedal

Part of: Volume: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (CSL 2011)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: Computer Science Logic (CSL)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2011-08-31

PDF

File

PDF

LIPIcs.CSL.2011.512.pdf

Filesize: 0.54 MB
13 pages

Document Identifiers

DOI: 10.4230/LIPIcs.CSL.2011.512
URN: urn:nbn:de:0030-drops-32535

Subject Classification

Keywords

countable choice
lambda calculus
program equivalence

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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

Cite As Get BibTex

Jan Schwinghammer and Lars Birkedal. Step-Indexed Relational Reasoning for Countable Nondeterminism. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 512-524, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011) https://doi.org/10.4230/LIPIcs.CSL.2011.512

Author Details

Jan Schwinghammer

Lars Birkedal

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail