new paper: A Relevant Analysis of Natural Deduction
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
participants (1)
-
Samin Ishtiaq