We present a fully abstract and effectively presentable model of unary FPC (a version of FPC with lifting rather than lifted sums) in a category of bicpos and continuous and stable functions. We show universality for the corresponding model of unary PCF, and then show that this implies full abstraction for unary FPC. We use a translation into this metalanguage to show that the $canonical" bidomain model of the lazy λ-calculus (with seqential convergence testing) is fully abstract.
|Title of host publication||Typed Lambda Calculi and Applications|
|Subtitle of host publication||Proceedings of 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003|
|Place of Publication||Berlin, Germany|
|Number of pages||15|
|Publication status||Published - 27 May 2003|
|Name||Lecture Notes in Computer Science|