Step-Indexed Relational Reasoning for Countable Nondeterminism

Lars Birkedal; Aleš Bizjak; Jan Schwinghammer

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

Lars Birkedal ; Aleš Bizjak ; Jan Schwinghammer - Step-Indexed Relational Reasoning for Countable Nondeterminism

lmcs:940 - Logical Methods in Computer Science, October 15, 2013, Volume 9, Issue 4 - https://doi.org/10.2168/LMCS-9(4:4)2013

Step-Indexed Relational Reasoning for Countable NondeterminismArticle

Authors: Lars Birkedal ; Aleš Bizjak ; Jan Schwinghammer

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}.

https://doi.org/10.2168/LMCS-9(4:4)2013

Source: arXiv.org:1310.2031

Volume: Volume 9, Issue 4

Published on: October 15, 2013

Imported on: March 6, 2012

Keywords: Computer Science - Logic in Computer Science

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

12 Documents citing this article

Alejandro Aguirre;Lars Birkedal, 2023, Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice, Proceedings of the ACM on Programming Languages, 7, POPL, pp. 33-60, 10.1145/3571195, https://doi.org/10.1145/3571195.

Arthur Charguéraud;Adam Chlipala;Andres Erbsen;Samuel Gruetter, 2023, Omnisemantics: Smooth Handling of Nondeterminism, ACM Transactions on Programming Languages and Systems, 45, 1, pp. 1-43, 10.1145/3579834, https://doi.org/10.1145/3579834.

Dániel Horpácsi;Péter Bereczky;Simon Thompson, 2023, Program equivalence in an untyped, call-by-value functional language with uncurried functions, Journal of Logical and Algebraic Methods in Programming, 132, pp. 100857, 10.1016/j.jlamp.2023.100857, https://doi.org/10.1016/j.jlamp.2023.100857.

Rasmus Ejlers Møgelberg;Andrea Vezzosi, 2021, Two Guarded Recursive Powerdomains for Applicative Simulation, arXiv (Cornell University), 351, pp. 200-217, 10.4204/eptcs.351.13.

Simon Spies;Lennard Gäher;Daniel Gratzer;Joseph Tassarotti;Robbert Krebbers;et al., Radboud Repository (Radboud University), Transfinite Iris: resolving an existential dilemma of step-indexed separation logic, pp. 80-95, 2021, Virtual Canada, 10.1145/3453483.3454031, https://repository.ubn.ru.nl//bitstream/handle/2066/236635/236635.pdf.

Simon Spies;Neel Krishnaswami;Derek Dreyer, 2021, Transfinite step-indexing for termination, Proceedings of the ACM on Programming Languages, 5, POPL, pp. 1-29, 10.1145/3434294, https://doi.org/10.1145/3434294.

Joseph Tassarotti;Ralf Jung;Robert Harper, arXiv (Cornell University), A Higher-Order Logic for Concurrent Termination-Preserving Refinement, pp. 909-936, 2017, 10.1007/978-3-662-54434-1_34, https://arxiv.org/abs/1701.05888.

Kasper Svendsen;Filip Sieczkowski;Lars Birkedal, Transfinite Step-Indexing: Decoupling Concrete and Logical Steps, pp. 727-751, 2016, 10.1007/978-3-662-49498-1_28, https://hal.inria.fr/hal-01408649.

Aleš Bizjak;Lars Birkedal, Lecture notes in computer science, Step-Indexed Logical Relations for Probability, pp. 279-294, 2015, 10.1007/978-3-662-46678-0_18, https://doi.org/10.1007/978-3-662-46678-0_18.

Aleš Bizjak;Lars Birkedal;Marino Miculan, Lecture notes in computer science, A Model of Countable Nondeterminism in Guarded Type Theory, pp. 108-123, 2014, 10.1007/978-3-319-08918-8_8.

Andrew Cave;Francisco Ferreira;Prakash Panangaden;Brigitte Pientka, CiteSeer X (The Pennsylvania State University), Fair reactive programming, 2014, San Diego California USA, 10.1145/2535838.2535881, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.405.856.

Andrew Cave;Francisco Ferreira;Prakash Panangaden;Brigitte Pientka, 2014, Fair reactive programming, ACM SIGPLAN Notices, 49, 1, pp. 361-372, 10.1145/2578855.2535881, https://doi.org/10.1145/2578855.2535881.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 2026 times.

This article's PDF has been downloaded 337 times.