Please use this identifier to cite or link to this item:
Title: Nominal lambda calculus: An internal language for FM-cartesian closed categories
Authors: Crole, Roy L.
Nebel, Frank
First Published: 11-Nov-2013
Presented at: Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics, MFPS XXIX
Publisher: Elsevier
Citation: Electronic Notes in Theoretical Computer Science, 2013, 298, pp. 93-117 Proceedings of the Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics, MFPS XXIX
Abstract: Reasoning about atoms (names) is difficult. The last decade has seen the development of numerous novel techniques. For equational reasoning, Clouston and Pitts introduced Nominal Equational Logic (NEL), which provides judgements of equality and freshness of atoms. Just as Equational Logic (EL) can be enriched with function types to yield the lambda-calculus (LC), we introduce NLC by enriching NEL with (atom-dependent) function types and abstraction types. We establish meta-theoretic properties of NLC; define -cartesian closed categories, hence a categorical semantics for NLC; and prove soundness & completeness by way of NLC-classifying categories. A corollary of these results is that NLC is an internal language for -cccs. A key feature of NLC is that it provides a novel way of encoding freshness via dependent types, and a new vehicle for studying the interaction of freshness and higher order types. © 2013 Elsevier B.V.
DOI Link: 10.1016/j.entcs.2013.09.009
ISSN: 1571-0661
Version: Publisher Version
Status: Peer-reviewed
Type: Conference Paper
Rights: © 2013 Elsevier B.V. Open access under CC BY-NC-ND license.
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
1-s2.0-S1571066113000558-main.pdfPublished (publisher PDF)435.59 kBAdobe PDFView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.