Loading...
Please wait, while we are loading the content...
Similar Documents
Curry--Howard terms for Linear Logic (1994)
| Content Provider | CiteSeerX |
|---|---|
| Author | Frank, David Albrecht Bauerle, Frank A. Crossley, John N. Jeavons, John S. |
| Description | 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. 1 |
| File Format | |
| Language | English |
| Publisher Date | 1994-01-01 |
| Publisher Institution | In Logic Colloquium |
| Access Restriction | Open |
| Subject Keyword | Full System Full First-order Linear Logic Natural Deduction System Curry Howard Term Linear Logic Curry Howard Style Term Term Variable Proof Net Reduction Rule Strong Normalization Curry-howard Term |
| Content Type | Text |
| Resource Type | Article |