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.

翻译：我们研究名义多排序签名的一种扩展，其中抽象具有一种称为广义具体化的实例化形式，作为消除运算符（类似于λ演算）。表达式随后使用一种尊重α转换（类似于依赖类型λ演算）但不允许名称携带抽象排序的排序与排序族系统进行分类，从而构成一个一阶依赖排序系统。该系统能够表示多种有趣演算的判断形式与推理规则。我们提出了该系统的规则与性质以及表示实验，并讨论了它如何构成构建类型理论的基础，其中具有α等价的原始表达式可得到完全形式化的处理。