A dependent nominal type theory

TL;DR

This paper introduces a dependent type theory incorporating nominal techniques, proving key properties like soundness and decidability, and discusses extensions for recursion and induction.

Contribution

It presents the first LF-style dependent type theory with name-abstraction types, establishing foundational properties and exploring extensions.

Findings

Proved soundness and decidability of beta-eta-equivalence

Demonstrated adequacy and canonical forms with examples

Discussed extensions like recursion and induction principles

Abstract

Nominal abstract syntax is an approach to representing names and binding pioneered by Gabbay and Pitts. So far nominal techniques have mostly been studied using classical logic or model theory, not type theory. Nominal extensions to simple, dependent and ML-like polymorphic languages have been studied, but decidability and normalization results have only been established for simple nominal type theories. We present a LF-style dependent type theory extended with name-abstraction types, prove soundness and decidability of beta-eta-equivalence checking, discuss adequacy and canonical forms via an example, and discuss extensions such as dependently-typed recursion and induction principles.