Representation and duality of the untyped λ-calculus in nominal lattice and topological semantics, with a proof of topological completeness

Jamie Gabbay; Michael Gabbay

doi:10.1016/j.apal.2016.10.001

Representation and duality of the untyped λ-calculus in nominal lattice and topological semantics, with a proof of topological completeness

Jamie Gabbay, Michael Gabbay

Research output: Contribution to journal › Article › peer-review

5 Citations (Scopus)

63 Downloads (Pure)

Abstract

We give a semantics for the λ-calculus based on a topological duality theorem in nominal sets. A novel interpretation of λ is given in terms of adjoints, and λ-terms are interpreted absolutely as sets (no valuation is necessary).

Original language	English
Pages (from-to)	501–621
Number of pages	121
Journal	Annals of Pure and Applied Logic
Volume	168
Issue number	3
Early online date	8 Oct 2016
DOIs	https://doi.org/10.1016/j.apal.2016.10.001
Publication status	Published - Mar 2017

Access to Document

10.1016/j.apal.2016.10.001

Download pdfAccepted author manuscript, 1.31 MBLicence: CC BY-NC-ND

Jamie Gabbay
- m.gabbayhw.acuk
- School of Mathematical & Computer Sciences - Assistant Professor
- School of Mathematical & Computer Sciences, Computer Science - Assistant Professor
Person: Academic (Research & Teaching)

Cite this

@article{04030a3d77ad4bfca276e69be4a111e5,

title = "Representation and duality of the untyped λ-calculus in nominal lattice and topological semantics, with a proof of topological completeness",

abstract = "We give a semantics for the λ-calculus based on a topological duality theorem in nominal sets. A novel interpretation of λ is given in terms of adjoints, and λ-terms are interpreted absolutely as sets (no valuation is necessary).",

author = "Jamie Gabbay and Michael Gabbay",

year = "2017",

month = mar,

doi = "10.1016/j.apal.2016.10.001",

language = "English",

volume = "168",

pages = "501–621",

journal = "Annals of Pure and Applied Logic",

issn = "0168-0072",

publisher = "Elsevier",

number = "3",

}

TY - JOUR

T1 - Representation and duality of the untyped λ-calculus in nominal lattice and topological semantics, with a proof of topological completeness

AU - Gabbay, Jamie

AU - Gabbay, Michael

PY - 2017/3

Y1 - 2017/3

N2 - We give a semantics for the λ-calculus based on a topological duality theorem in nominal sets. A novel interpretation of λ is given in terms of adjoints, and λ-terms are interpreted absolutely as sets (no valuation is necessary).

AB - We give a semantics for the λ-calculus based on a topological duality theorem in nominal sets. A novel interpretation of λ is given in terms of adjoints, and λ-terms are interpreted absolutely as sets (no valuation is necessary).

U2 - 10.1016/j.apal.2016.10.001

DO - 10.1016/j.apal.2016.10.001

M3 - Article

SN - 0168-0072

VL - 168

SP - 501

EP - 621

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

IS - 3

ER -

Representation and duality of the untyped λ-calculus in nominal lattice and topological semantics, with a proof of topological completeness

Abstract

Access to Document

Fingerprint

Profiles

Jamie Gabbay

Cite this