Sequential Functions on Indexed Domains and Full Abstraction for a Sub-Language of PCF,

We present a general semantic framework of sequential functions on domains equipped with a parameterized notion of incremental sequential computation. Under the simplifying assumption that computation other function spaces proceeds by successive application to constants, we construct a sequential semantic model for a non-trivial sub-language of PCF with a corresponding syntactic restriction - that variables of function type may only be applied to closed terms. We show that the model is fully abstract for the sub-language, with respect to the usual notion of program behavior.