Light Logics and the Call-by-Value Lambda Calculus
The so-called light logics have been introduced as logical systems enjoying quite remarkable normalization properties. Designing a type assignment system for pure lambda calculus from these logics, however, is problematic. In this paper we show that shifting from usual call-by-name to call-by-value...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2008-11-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/820/pdf |
| _version_ | 1797268796184985600 |
|---|---|
| author | Paolo Coppola Ugo Dal Lago Simona Ronchi Della Rocca |
| author_facet | Paolo Coppola Ugo Dal Lago Simona Ronchi Della Rocca |
| author_sort | Paolo Coppola |
| collection | DOAJ |
| description | The so-called light logics have been introduced as logical systems enjoying
quite remarkable normalization properties. Designing a type assignment system
for pure lambda calculus from these logics, however, is problematic. In this
paper we show that shifting from usual call-by-name to call-by-value lambda
calculus allows regaining strong connections with the underlying logic. This
will be done in the context of Elementary Affine Logic (EAL), designing a type
system in natural deduction style assigning EAL formulae to lambda terms. |
| first_indexed | 2024-04-25T01:38:10Z |
| format | Article |
| id | doaj.art-d1a68186c36a4b859de366bb40eb085a |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:38:10Z |
| publishDate | 2008-11-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-d1a68186c36a4b859de366bb40eb085a2024-03-08T08:57:54ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742008-11-01Volume 4, Issue 410.2168/LMCS-4(4:5)2008820Light Logics and the Call-by-Value Lambda CalculusPaolo CoppolaUgo Dal Lagohttps://orcid.org/0000-0001-9200-070XSimona Ronchi Della RoccaThe so-called light logics have been introduced as logical systems enjoying quite remarkable normalization properties. Designing a type assignment system for pure lambda calculus from these logics, however, is problematic. In this paper we show that shifting from usual call-by-name to call-by-value lambda calculus allows regaining strong connections with the underlying logic. This will be done in the context of Elementary Affine Logic (EAL), designing a type system in natural deduction style assigning EAL formulae to lambda terms.https://lmcs.episciences.org/820/pdfcomputer science - logic in computer sciencef.4.1 |
| spellingShingle | Paolo Coppola Ugo Dal Lago Simona Ronchi Della Rocca Light Logics and the Call-by-Value Lambda Calculus Logical Methods in Computer Science computer science - logic in computer science f.4.1 |
| title | Light Logics and the Call-by-Value Lambda Calculus |
| title_full | Light Logics and the Call-by-Value Lambda Calculus |
| title_fullStr | Light Logics and the Call-by-Value Lambda Calculus |
| title_full_unstemmed | Light Logics and the Call-by-Value Lambda Calculus |
| title_short | Light Logics and the Call-by-Value Lambda Calculus |
| title_sort | light logics and the call by value lambda calculus |
| topic | computer science - logic in computer science f.4.1 |
| url | https://lmcs.episciences.org/820/pdf |
| work_keys_str_mv | AT paolocoppola lightlogicsandthecallbyvaluelambdacalculus AT ugodallago lightlogicsandthecallbyvaluelambdacalculus AT simonaronchidellarocca lightlogicsandthecallbyvaluelambdacalculus |