A fully abstract bidomain model of unary FPC

Research output: Chapter or section in a book/report/conference proceedingChapter or section

4 Citations (SciVal)


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.

Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications
Subtitle of host publicationProceedings of 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003
EditorsM. Hofmann
Place of PublicationBerlin, Germany
PublisherSpringer Verlag
Number of pages15
ISBN (Print)9783540403326
Publication statusPublished - 27 May 2003

Publication series

NameLecture Notes in Computer Science


Dive into the research topics of 'A fully abstract bidomain model of unary FPC'. Together they form a unique fingerprint.

Cite this