We give a simple order-theoretic construction of a cartesian closed category of sequential functions. It is based on biordered sets analogous to Berry's bidomains, except that the stable order is replaced with a new notion, the bistable order, and instead of preserving stably bounded greatest lower bounds, functions are required to preserve bistably bounded least upper bounds and greatest lower bounds. We show that bistable epos and bistable and continuous functions form a CCC, yielding models of functional languages such as the simply-typed λ-calculus and SPCF. We show that these models are strongly sequential and use this fact to prove universality and full abstraction results. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Laird, J. (2003). Bistability: An extensional characterization of sequentiality. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2803, 372–383. https://doi.org/10.1007/978-3-540-45220-1_30
Mendeley helps you to discover research relevant for your work.