Abstract

In their LICS paper, J. Riecke and A. Sandholm constructed a domain theoretic model for FPC, a call-by-value language containing recursive types and sum types. I will generalise their approach by presenting a cartesian closed category SD of domains that contains Riecke and Sandholm's model as a subcategory.

Next, I shall present a universal language SFL (sequential functional language) containing recursive types various kinds of product types, sum types and function types. This language can be used as a metalanguage for different sequential languages, in particular call-by-value and call-by-name ones.

Finally, I will show that the category SD provides a fully abstract model for SFL.