# new paper: A Relevant Analysis of Natural Deduction

• To: types@cs.indiana.edu
• Subject: new paper: A Relevant Analysis of Natural Deduction
• From: Samin Ishtiaq <si@dcs.qmw.ac.uk>
• Date: Tue, 24 Feb 1998 14:18:08 GMT
• Delivery-Date: Tue, 24 Feb 1998 09:18:37 -0500

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