[Prev][Next][Index][Thread]

new paper: A Relevant Analysis of Natural Deduction

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