Dependently Sorted Nominal Signatures
Maribel Fernández, Miguel Pagano, Nora Szasz, Álvaro Tasistro
TL;DR
This work extends Pitts' nominal signatures with dependently sorted types, yielding a first-order yet alpha-equivalence-respecting framework built on generalised concretion to model abstraction elimination. It demonstrates how First Order Logic and Lambda Calculi can be represented and reasoned about within this framework, including shallow and deep encodings and adequacy proofs that link object-language derivations to meta-level terms. The approach enables formal treatment of raw expressions modulo alpha-equivalence and points toward a nominal type theory with binding handled at the infrastructural level. The results suggest a versatile logical framework for specifying and reasoning about languages with binding, with potential applications to formalizing type theories and computation in a alpha-aware setting.
Abstract
We investigate an extension of nominal many-sorted signatures in which abstraction has a form of instantiation, called generalised concretion, as elimination operator (similarly to lambda-calculi). Expressions are then classified using a system of sorts and sort families that respects alpha-conversion (similarly to dependently-typed lambda-calculi) but not allowing names to carry abstraction sorts, thus constituting a first-order dependent sort system. The system can represent forms of judgement and rules of inference of several interesting calculi. We present rules and properties of the system as well as experiments of representation, and discuss how it constitutes a basis on which to build a type theory where raw expressions with alpha-equivalence are given a completely formal treatment.