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

  • Full text (.ps).
  • Extended Abstract (.ps) presented at TLCA '03.
  • Slides (.ps) from a presentation of this work.
  • Bibtex entry
    author = "J. Laird",
    title = "Sequentiality in Bounded Bidomains",
    journal = "Fundamenta Informaticae",
    volume = 65,
    pages = "173 -- 191",
    publisher = "IOS press",
    year = 2005}