[Prev][Next][Index][Thread]
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

DeliveryDate: 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 firstorder 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 judgementsastypes,
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
propositionastypes correspondence and a Gentzenization of the type
theory. We are also investigating categorical models, specifically
resourcedindexed Kripke models, of the
$\lambda\Lambda_{\kappa}$calculus.
Samin Ishtiaq
David Pym