Curry-Howard Terms for Linear Logic |
| |
| Authors: | Bäuerle Frank A Albrecht David Crossley John N Jeavons John S |
| |
| Institution: | (1) Department of Mathematics, University of California, Santa Cruz, CA, USA;(2) Department of Computer Science, Monash University, Melbourne, Australia;(3) Department of Mathematics, Monash University, Melbourne, Australia |
| |
| Abstract: | In this paper we 1. provide a natural deduction system for full first-order linear logic, 2. introduce Curry-Howard-style terms for this version of linear logic, 3. extend the notion of substitution of Curry-Howard terms for term variables, 4. define the reduction rules for the Curry-Howard terms and 5. outline a proof of the strong normalization for the full system of linear logic using a development of Girard's candidates for reducibility, thereby providing an alternative to Girard's proof using proof-nets. |
| |
| Keywords: | linear logic Curry-Howard terms strong normalization |
| 本文献已被 SpringerLink 等数据库收录！ |
|
