text: We offer a short tour into the interactive interpretation of sequential programs. We emphasize streamlike computation — that is, computation of successive bits of information upon request. The core of the approach surveyed here dates back to the work of Berry and the author on sequential algorithms on concrete data structures in the late seventies, culminating in the design of the programming language CDS, in which the semantics of programs of any type can be explored interactively. Around one decade later, two major insights of Cartwright and Felleisen on one hand, and of Lamarche on the other hand gave new, decisive impulses to the study of sequentiality. Cartwright and Felleisen observed that sequential algorithms give a direct semantics to control operators like call-cc and proposed to include explicit errors both in the syntax and in the semantics of the language PCF. Lamarche (unpublished) connected sequential algorithms to linear logic and games. The successful program of games semantics has spanned over the nineties until now, starting with syntax-independent characterizations of the term model of PCF by Abramsky, Jagadeesan, and Malacaria on one hand, and by Hyland and Ong on the other hand.
  @cite_16: We prove that, in the hierarchy of simple types based on the type of natural numbers, any finite strongly stable function is equal to the application of the semantics of a PCF-definable functional to some strongly stable (generally not PCF-definable) functionals of type two. Applying a logical relation technique, we derive from this result that the strongly stable model of PCF is the extensional collapse of its sequential algorithms model.
  @cite_10: In the previous chapter, we saw how the model PC offers a ‘maximal’ class of partial computable functionals strictly extending SF (in the sense of the poset ( J ( N _ ) ) of Subsection 3.6.4). In the present chapter, we show that SF can also be extended in a very different direction to yield another class SR of ‘computable’ functionals which is in some sense incompatible with PC. This class was first identified by Bucciarelli and Ehrhard [45] as the class of strongly stable functionals; later work by Ehrhard [69], van Oosten [294] and Longley [176] established the computational significance of these functionals, investigated their theory in some detail, and provided a range of alternative characterizations.
  @cite_3: We present a cartesian closed category of dI-domains with coherence and strongly stable functions which provides a new model of PCF, where terms are interpreted by functions and where, at first order, all functions are sequential. We show how this model can be refined in such a way that the theory it induces on the terms of PCF be strictly finer than the theory induced by the Scott model of continuous functions.
summary: Two important models of functions that have been constructed since turned out to be the extensional collapse (i.e. the hereditary quotient equating sequential algorithms computing the same function, i.e. (in the affine case) two algorithms @math and @math such that @math ): Bucciarelli and Ehrhard's model of strongly stable functions @cite_3 @cite_16 , and Longley's model of sequentially realizable functionals @cite_10 . The first model arose from an algebraic characterization of sequential (first-order) functions, that carries over to all types. The second one is a realizability model over a combinatory algebra in which the interaction at work in sequential algorithms is encoded.