A Simple Nominal Type Theory

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

Nominal logic is an extension of first-order logic with features useful for reasoning about abstract syntax with bound names. For computational applications such as programming and formal reasoning, it is desirable to develop constructive type theories for nominal logic that extend standard type theories for propositional, first- or higher-order logic. This has proven difficult, largely because of complex interactions between nominal logic's name-abstraction operation and ordinary functional abstraction. This difficulty already arises in the case of propositional logic and simple type theory. In this paper we show how this difficulty can be overcome, and present a simple nominal type theory that enjoys properties such as type soundness and strong normalization, and that can be soundly interpreted using existing nominal set models of nominal logic. We also sketch how recursion combinators for languages with binding structure can be provided. This is a first step towards understanding the constructive content of nominal logic and incorporating it into existing constructive logics and type theories.
Original languageEnglish
Pages (from-to)37 - 52
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Volume228
Issue number0
DOIs
Publication statusPublished - Jan 2009

Keywords / Materials (for Non-textual outputs)

  • type systems

Fingerprint

Dive into the research topics of 'A Simple Nominal Type Theory'. Together they form a unique fingerprint.

Cite this