A fully abstract bidomain model of unary FPC

Research output: Chapter in Book/Report/Conference proceedingChapter

4 Citations (Scopus)

Abstract

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
Pages211-225
Number of pages15
ISBN (Print)9783540403326
DOIs
Publication statusPublished - 27 May 2003

Publication series

NameLecture Notes in Computer Science
Volume2701

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

  • Cite this

    Laird, J. (2003). A fully abstract bidomain model of unary FPC. In M. Hofmann (Ed.), Typed Lambda Calculi and Applications: Proceedings of 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 (pp. 211-225). (Lecture Notes in Computer Science; Vol. 2701). Springer Verlag. https://doi.org/10.1007/3-540-44904-3_15