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

Unary
Canonical Model
Lambda Calculus
Universality
Model
Imply
Testing

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). Berlin, Germany: Springer Verlag. https://doi.org/10.1007/3-540-44904-3_15

A fully abstract bidomain model of unary FPC. / Laird, Jim.

Typed Lambda Calculi and Applications: Proceedings of 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 . ed. / M. Hofmann. Berlin, Germany : Springer Verlag, 2003. p. 211-225 (Lecture Notes in Computer Science; Vol. 2701).

Research output: Chapter in Book/Report/Conference proceedingChapter

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 . Lecture Notes in Computer Science, vol. 2701, Springer Verlag, Berlin, Germany, pp. 211-225. https://doi.org/10.1007/3-540-44904-3_15
Laird J. A fully abstract bidomain model of unary FPC. In Hofmann M, editor, Typed Lambda Calculi and Applications: Proceedings of 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 . Berlin, Germany: Springer Verlag. 2003. p. 211-225. (Lecture Notes in Computer Science). https://doi.org/10.1007/3-540-44904-3_15
Laird, Jim. / A fully abstract bidomain model of unary FPC. Typed Lambda Calculi and Applications: Proceedings of 6th International Conference, TLCA 2003 Valencia, Spain, June 10–12, 2003 . editor / M. Hofmann. Berlin, Germany : Springer Verlag, 2003. pp. 211-225 (Lecture Notes in Computer Science).
@inbook{779864744dc641ecb6a6a55a1a3f4781,
title = "A fully abstract bidomain model of unary FPC",
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.",
author = "Jim Laird",
year = "2003",
month = "5",
day = "27",
doi = "10.1007/3-540-44904-3_15",
language = "English",
isbn = "9783540403326",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "211--225",
editor = "M. Hofmann",
booktitle = "Typed Lambda Calculi and Applications",

}

TY - CHAP

T1 - A fully abstract bidomain model of unary FPC

AU - Laird, Jim

PY - 2003/5/27

Y1 - 2003/5/27

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33645475503&partnerID=8YFLogxK

UR - http://dx.doi.org/10.1007/3-540-44904-3_15

U2 - 10.1007/3-540-44904-3_15

DO - 10.1007/3-540-44904-3_15

M3 - Chapter

SN - 9783540403326

T3 - Lecture Notes in Computer Science

SP - 211

EP - 225

BT - Typed Lambda Calculi and Applications

A2 - Hofmann, M.

PB - Springer Verlag

CY - Berlin, Germany

ER -