Sequential functions on indexed domains and full abstraction for a sub-language of PCF

Steven Brookes
Shai Geva

CMU SCS Tech reports 93-163, School of Computer Science, Carnegie Mellon University, 1993
In Mathematical Foundations of Programming Semantics, Proceedings of the Ninth International Conference, MFPS '93, New Orleans, April 1993. Lecture Notes in Computer Science, vol 802. Springer-Verlag

Available as PostScript.

Abstract:

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



[BRICS symbol] BRICS WWW home page