A relevant analysis of natural deduction

Abstract
We study a framework, RLF, for defining natural deduction presentations of linear and other relevant logics. RLF consists in a language together, in a manner similar to that of LF, with a representation mechanism. The language of RLF, the λλκ-calculus, is a system of first-order linear dependent function types which uses a function κ to describe the degree of sharing of variables between functions and their arguments. The representation mechanism is judgements-as-types, developed for linear and other relevant logics. The λλκ-calculus is a conservative extension of the λΠ-calculus and RLF is a conservative extension of LF.