Nominal Lambda Calculus

Since their introduction, nominal techniques have been widely applied in computer science to reason about syntax of formal systems involving name-binding operators. The work in this thesis is in the area of “nominal" type theory, or more precisely the study of “nominal" simple types. We take Nominal Equational Logic (NEL), which augments equational logic with freshness judgements, as our starting point to introduce the Nominal Lambda Calculus (NLC), a typed lambda calculus that provides a simple form of name-dependent function types. This is a key feature of NLC, which allows us to encode freshness in a novel way. We establish meta-theoretic properties of NLC and introduce a sound model theoretic semantics. Further, we introduce NLC[A], an extension of NLC that captures name abstraction and concretion, and provide pure NLC[A] with a strongly normalising and confluent βη-reduction system. A property that has not yet been studied for “nominal" typed lambda calculi is completeness of βη-conversion for a nominal analogue of full set-theoretic hierarchies. Aiming towards such a result, we analyse known proof techniques and identify various issues. As an interesting precursor, we introduce full nominal hierarchies and demonstrate that completeness holds for βη-conversion of the ordinary typed lambda calculus. The notion of FM-categories was developed by Ranald Clouston to demonstrate that FM-categories correspond precisely to NEL-theories. We augment FM-categories with equivariant exponentials and show that they soundly model NLC-theories. We then outline why NLC is not complete for such categories, and discuss in detail an approach towards extending NLC which yields a promising framework from which we aim to develop a future (sound and complete) categorical semantics and a categorical type theory correspondence. Moreover, in pursuit of a categorical conservative extension result, we study (enriched/ internal) Yoneda isomorphisms for “nominal" categories and some form of “nominal" gluing.