We apologize for multiple copies of this mail. The following paper will appear in the Journal of Logic and Computation (expected in Vol. 8) later this year: A Relevant Analysis of Natural Deduction S Ishtiaq and DJ Pym Queen Mary and Westfield College University of London {si,pym}@dcs.qmw.ac.uk 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 $\lambda\Lambda_{\kappa}$-calculus, is a system of first-order linear dependent function types which uses a function $\kappa$ 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 $\lambdal\Lambda_{\kappa}$-calculus is a conservative extension of the $\lambda\Pi$-calculus and RLF is a conservative extension of LF. The paper will be available from our Hypatia entries, at http://hypatia.dcs.qmw.ac.uk. It is also available at http://www.dcs.qmw.ac.uk/~si. We are currently engaged in further study of the proof theory of the $\lambda\Lambda_{\kappa}$-calculus; this includes setting up a proposition-as-types correspondence and a Gentzenization of the type theory. We are also investigating categorical models, specifically resourced-indexed Kripke models, of the $\lambda\Lambda_{\kappa}$-calculus. Samin Ishtiaq David Pym