Indexed Linear Logic has been introduced by Ehrhard and Bucciarelli, it can be seen as a logical presentation of non-idempotent intersection types extended through the relational semantics to the full linear logic. We introduce an idempotent variant of Indexed Linear Logic. We give a fine-grained reformulation of the syntax by exposing implicit parameters and by unifying several operations on formulae via the notion of base change. Idempotency is achieved by means of an appropriate subtyping relation. We carry on an in-depth study of indLL as a logic, showing how it determines a refinement of classical linear logic and establishing a terminating cut-elimination procedure. Cut-elimination is proved to be confluent up to an appropriate congruence induced by the subtyping relation.

翻译：索引线性逻辑由Ehrhard和Bucciarelli提出，可视为非幂等交集类型通过关系语义扩展至完整线性逻辑的逻辑表述。我们引入索引线性逻辑的幂等变体。通过暴露隐式参数并借助基变换概念统一公式上的若干操作，对语法进行了细粒度重构。幂等性通过适当的子类型关系实现。我们深入研究了indLL作为逻辑的性质，揭示其如何确定经典线性逻辑的精化，并建立了可终止的切割消除过程。切割消除被证明在由子类型关系导出的适当同余关系下具有合流性。