Computer Science – Programming Languages
Scientific paper
2007-02-28
LMCS 3 (2:5) 2007
Computer Science
Programming Languages
To appear in LMCS
Scientific paper
10.2168/LMCS-3(2:5)2007
We give a simple order-theoretic construction of a Cartesian closed category of sequential functions. It is based on bistable biorders, which are sets with a partial order -- the extensional order -- and a bistable coherence, which captures equivalence of program behaviour, up to permutation of top (error) and bottom (divergence). We show that monotone and bistable functions (which are required to preserve bistably bounded meets and joins) are strongly sequential, and use this fact to prove universality results for the bistable biorder semantics of the simply-typed lambda-calculus (with atomic constants), and an extension with arithmetic and recursion. We also construct a bistable model of SPCF, a higher-order functional programming language with non-local control. We use our universality result for the lambda-calculus to show that the semantics of SPCF is fully abstract. We then establish a direct correspondence between bistable functions and sequential algorithms by showing that sequential data structures give rise to bistable biorders, and that each bistable function between such biorders is computed by a sequential algorithm.
No associations
LandOfFree
Bistable Biorders: A Sequential Domain Theory does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Bistable Biorders: A Sequential Domain Theory, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Bistable Biorders: A Sequential Domain Theory will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-524685