Abstract
The so-called light logics [1,2,3] 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, as discussed in [4]. 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.
The three authors are partially supported by PRIN projects PROTOCOLLO (2002) and FOLLIA (2004).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Girard, J.Y.: Light linear logic. Information and Computation 143(2), 175–204 (1998)
Asperti, A.: Light affine logic. In: Proceedings of the 13th IEEE Syposium on Logic in Computer Science, pp. 300–308 (1998)
Asperti, A., Roversi, L.: Intuitionistic light affine logic. ACM Transactions on Computational Logic 3(1), 137–175 (2002)
Baillot, P., Terui, K.: Light types for polynomial time computation in lambda-calculus. In: Proceedings of the 19th IEEE Syposium on Logic in Computer Science, pp. 266–275 (2004)
Coppola, P., Martini, S.: Typing lambda terms in elementary logic with linear constraints. In: Proceedings of the 6th International Conference on Typed Lambda-Calculus and Applications, pp. 76–90 (2001)
Coppola, P., Ronchi della Rocca, S.: Principal typing in elementary affine logic. In: Proceedings of the 7th International Conference on Typed Lambda-Calculus and Applications, pp. 90–104 (2003)
Terui, K.: Light affine lambda calculus and polytime strong normalization. In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science, pp. 209–220 (2001)
Terui, K.: Light logic and polynomial time computation. PhD thesis, Keio University (2002)
Baillot, P.: Checking polynomial time complexity with types. In: Proceedings of the 2nd IFIP International Conference on Theoretical Computer Science (2002)
Coppola, P., Martini, S.: Optimizing optimal reduction, a type inference algorithm for elementary affine logic. ACM Transactions on Computational Logic (2004) (To appear)
Baillot, P., Mogbil, V.: Soft lambda-calculus: a language for polynomial time computation. In: Proceedings of the 7th International Conference on Foundations of Software Science and Computational Structures (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coppola, P., Dal Lago, U., Della Rocca, S.R. (2005). Elementary Affine Logic and the Call-by-Value Lambda Calculus. In: Urzyczyn, P. (eds) Typed Lambda Calculi and Applications. TLCA 2005. Lecture Notes in Computer Science, vol 3461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11417170_11
Download citation
DOI: https://doi.org/10.1007/11417170_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25593-2
Online ISBN: 978-3-540-32014-2
eBook Packages: Computer ScienceComputer Science (R0)