A Relational Account of Call-by-Value Sequentiality

We construct a model for FPC, a purely functional, sequential, call-by-value language. The model is built from partial continuous functions, in the style of Plotkin, further constrained to be uniform with respect to a class of logical relations. We prove that the model is fully abstract. 1 Introduction The problem of finding an abstract description of sequential functional computation has been one of the most enduring problems of semantics. The problem dates from a seminal paper of Plotkin (1977), who pointed out that certain elements in Scott models are not definable. In Plotkin's example, the function por(x;y) = 8 < : true if x or y = true false if x and y = false ? otherwise where ? denotes divergence, cannot be programmed in the language PCF, a purely functional, sequential, call-byname language with booleans and numbers as base types. The problem is called the "sequentiality problem" because, intuitively, the only way to program por involves evaluating boolean expressions in p..