Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets

Murdoch J. Gabbay
Dominic P. Mulligan

We investigate a class of nominal algebraic Henkin-style models for the simply typed lambda-calculus in which variables map to names in the denotation and lambda-abstraction maps to a (non-functional) name-abstraction operation. The resulting denotations are smaller and better-behaved, in ways we make precise, than functional valuation-based models.

Using these new models, we then develop a generalisation of λ-term syntax enriching them with existential meta-variables, thus yielding a theory of incomplete functions. This incompleteness is orthogonal to the usual notion of incompleteness given by function abstraction and application, and corresponds to holes and incomplete objects.

In Herman Geuvers and Gopalan Nadathur: Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011), Nijmegen, The Netherlands, August 26, 2011, Electronic Proceedings in Theoretical Computer Science 71, pp. 58–75.
Published: 31st October 2011.

ArXived at: https://dx.doi.org/10.4204/EPTCS.71.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org