A fully abstract bidomain model of unary FPC

Jim Laird

doi:10.1007/3-540-44904-3_15

A fully abstract bidomain model of unary FPC

Jim Laird

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

4 Citations (SciVal)

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 language	English
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
Editors	M. Hofmann
Place of Publication	Berlin, Germany
Publisher	Springer Verlag
Pages	211-225
Number of pages	15
ISBN (Print)	9783540403326
DOIs	https://doi.org/10.1007/3-540-44904-3_15
Publication status	Published - 27 May 2003

Publication series

Name	Lecture Notes in Computer Science
Volume	2701

Access to Document

10.1007/3-540-44904-3_15

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

Cite this

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 or section in a book/report/conference proceeding › Chapter or section

@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 = may,

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 or section

AN - SCOPUS:33645475503

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 -

A fully abstract bidomain model of unary FPC

Abstract

Publication series

Access to Document

Other files and links

Fingerprint

Cite this