From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/658 Path: news.gmane.org!not-for-mail From: Samin Ishtiaq Newsgroups: gmane.science.mathematics.categories Subject: new paper: A Relevant Analysis of Natural Deduction Date: Tue, 24 Feb 1998 14:18:32 GMT Message-ID: <199802241418.OAA21711@wax.dcs.qmw.ac.uk> NNTP-Posting-Host: main.gmane.org X-Trace: ger.gmane.org 1241017103 26761 80.91.229.2 (29 Apr 2009 14:58:23 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 14:58:23 +0000 (UTC) To: categories@mta.ca Original-X-From: cat-dist Thu Feb 26 23:52:00 1998 Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.8.8/8.8.8) id WAA21381 for categories-list; Thu, 26 Feb 1998 22:07:44 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Original-Sender: cat-dist@mta.ca Precedence: bulk Original-Lines: 46 Xref: news.gmane.org gmane.science.mathematics.categories:658 Archived-At: 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