|
Edinburgh Research Archive >
Informatics, School of >
Informatics Report Series >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1842/3469
|
| Title: | Stratified coherent spaces: a denotational semantics for Light Linear Logic |
| Authors: | Baillot, Patrick |
| Issue Date: | Aug-2000 |
| Publisher: | The University of Edinburgh |
| Series/Report no.: | Informatics Report Series
EDI-INF-RR-0025 |
| Abstract: | Light linear logic (LLL) was introduced by Girard as a logical system capturing the class of polytime function within the proofs-as-programs approach. This paper deals with the denotational semantics of LLL: we introduce a variant of coherent spaces and prove that it is a sound model for this system, but not for usual linear logic. A simpler version of the model yields a sound semantics of Elementary linear logic, which is the analog of LLL for the class of Kalmar elementary functions. |
| Keywords: | Informatics |
| URI: | http://hdl.handle.net/1842/3469 |
| Appears in Collections: | Informatics Report Series
|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.
|
