* new paper: A Relevant Analysis of Natural Deduction
@ 1998-02-24 14:18 Samin Ishtiaq
0 siblings, 0 replies; only message in thread
From: Samin Ishtiaq @ 1998-02-24 14:18 UTC (permalink / raw)
To: categories
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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~1998-02-24 14:18 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
1998-02-24 14:18 new paper: A Relevant Analysis of Natural Deduction Samin Ishtiaq
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).