Affordable Access

Publisher Website

Nominal Lambda Calculus: An Internal Language for FM-Cartesian Closed Categories

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
298
Identifiers
DOI: 10.1016/j.entcs.2013.09.009
Keywords
  • Category Theory
  • Dependent Types
  • Fm-Sets
  • Internal Language
  • Nominal Logic
  • Semantics
  • Type Theory
Disciplines
  • Linguistics

Abstract

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.

There are no comments yet on this publication. Be the first to share your thoughts.