STEP-INDEXED RELATIONAL REASONING FOR COUNTABLE NONDETERMINISM

被引：12
作者：
Birkedal, Lars [1 ]
Bizjak, Ales [1 ]
Schwinghammer, Jan [2 ]
机构：
[1] Aarhus Univ, DK-8000 Aarhus C, Denmark
[2] Univ Saarland, D-66123 Saarbrucken, Germany
来源：
LOGICAL METHODS IN COMPUTER SCIENCE | 2013年 / 9卷 / 04期
关键词：
Countable choice; lambda calculus; program equivalence; RECURSIVE TYPES;
D O I：
10.2168/LMCS-9(4:4)2013
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页数：22
相关论文
共 20 条
[1]  
Agha G. A., 1997, Journal of Functional Programming, V7, P1, DOI 10.1017/S095679689700261X
[2]   An indexed model of recursive types for foundational proof-carrying code [J].
Appel, AW ;
McAllester, D .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001, 23 (05) :657-683
[3]   COUNTABLE NONDETERMINISM AND RANDOM ASSIGNMENT [J].
APT, KR ;
PLOTKIN, GD .
JOURNAL OF THE ACM, 1986, 33 (04) :724-767
[4]   Relational interpretations of recursive types an operational setting [J].
Birkedal, L ;
Harper, R .
INFORMATION AND COMPUTATION, 1999, 155 (1-2) :3-63
[5]   Step-Indexed Kripke Models over Recursive Worlds [J].
Birkedal, Lars ;
Reus, Bernhard ;
Schwinghammer, Jan ;
Stovring, Kristian ;
Thamsborg, Jacob ;
Yang, Hongseok .
ACM SIGPLAN NOTICES, 2011, 46 (01) :119-131
[6]  
Di Gianantonio P., 1995, Nordic Journal of Computing, V2, P126
[7]  
Di Gianantonio P, 2004, LECT NOTES COMPUT SC, V2987, P136
[8]   LOGICAL STEP-INDEXED LOGICAL RELATIONS [J].
Dreyer, Derek ;
Ahmed, Amal ;
Birkedal, Lars .
LOGICAL METHODS IN COMPUTER SCIENCE, 2011, 7 (02)
[9]   The Impact of Higher-Order State and Control Effects on Local Relational Reasoning [J].
Dreyer, Derek ;
Neis, Georg ;
Birkedal, Lars .
ACM SIGPLAN NOTICES, 2010, 45 (09) :143-155
[10]   A Generic Operational Metatheory for Algebraic Effects [J].
Johann, Patricia ;
Simpson, Alex ;
Voigtlaender, Janis .
25TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2010), 2010, :209-218
12