- 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.
- Copyright:
- 2000 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @Misc{EDI-INF-RR-0025,
- author = {
Patrick Baillot
},
- title = {Stratified coherent spaces: a denotational semantics for Light Linear Logic},
- year = 2000,
- month = {Aug},
- }
|
