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.
Light Logics and the Call-by-value Lambda Calculus / P. Coppola; U. Dal Lago; S. Ronchi Della Rocca. - In: LOGICAL METHODS IN COMPUTER SCIENCE. - ISSN 1860-5974. - ELETTRONICO. - 4 (4:5):(2008), pp. 1-28. [10.2168/LMCS-4(4:5)2008]
Light Logics and the Call-by-value Lambda Calculus
DAL LAGO, UGO;
2008
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
