Abstract
This note provides an example that demonstrates that in non-deterministic call-by-need lambda-calculi extended with cyclic let, extensionality as well as applicative bisimulation in general may not be used as criteria for contextual equivalence w.r.t. may- and two different forms of must-convergence. We also outline how the counterexample can be adapted to other calculi.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 711-716 |
| Number of pages | 6 |
| Journal | Information Processing Letters |
| Volume | 111 |
| Issue number | 14 |
| DOIs | |
| State | Published - Jul 31 2011 |
Bibliographical note
Copyright:Copyright 2011 Elsevier B.V., All rights reserved.
Keywords
- Contextual semantics
- Formal semantics
- Program correctness
- Programming calculi