(joint work with Tobias Loew)
The category OSA (of Observably Sequential Algorithms) was introduced in the early 1990ies by Cartwright, Curien and Felleisen and shown to give rise to a fully abstract model for SPCF.
We show that this model is also universal for the computable part of OSA because every type appears as SPCF definable retract of U = N --> N and all computable elements of U can be expressed in SPCF.
Moreover, when performing the D_\infty construction of D.Scott within OSA and starting from Sierpinski space O (containing only \bot and \top) then we get a minimal D in OSA which is isomorphic to all \omega-ary functions from D to O. We show that this structure gives rise to a universal model for an infinitary typed \lambda-calculus CPS_\infty (infinitary CPS target language) with an error element \top and infinitary application and abstraction.
Using this one gets a conceptual proof of a theorem of Laird saying that for simple types OSA is the quotient of innocent games modulo observational equivalence.