University of Leicester
Browse
1-s2.0-S1571066113000558-main.pdf (435.59 kB)

Nominal lambda calculus: An internal language for FM-cartesian closed categories

Download (435.59 kB)
conference contribution
posted on 2016-12-16, 15:17 authored by Roy L. Crole, Frank Nebel
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.

History

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

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science

Source

Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics, MFPS XXIX

Version

  • VoR (Version of Record)

Published in

Electronic Notes in Theoretical Computer Science

Publisher

Elsevier

issn

1571-0661

Copyright date

2013

Available date

2016-12-16

Publisher version

http://www.sciencedirect.com/science/article/pii/S1571066113000558

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC