Abstract
We study a notion of bounded stable biorder, showing that the monotone and stable functions on such biorders are sequential. We construct bounded biorder models of a range of sequential, higher-order functional calculi, including unary PCF, (typed and untyped) call-by-value and lazy λ-calculi, and non-deterministic SPCF. We prove universality and full abstraction results for these models by reduction to the case of unary PCF, for which we give a simple new argument to show that any order-extensional and sequential model is universal.
| Original language | English |
|---|---|
| Pages (from-to) | 173-191 |
| Number of pages | 19 |
| Journal | Fundamenta Informaticae |
| Volume | 65 |
| Issue number | 1-2 |
| Publication status | Published - 2005 |