Abstract
We present a type inference algorithm for λ-terms in Elementary Affine Logic using linear constraints. We prove that the algorithm is correct and complete.
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
Andrea Asperti. Light affine logic. In Proc. of the 13-th Annual IEEE Symposium on Logic in Computer Science (LICS’ 98), pages 300–308, Indianapolis, U.S.A., 1998.
Andrea Asperti, Paolo Coppola, and Simone Martini. (Optimal) duplication is not elementary recursive. In ACM POPL’00, pages 96–107, Boston, Massachusetts, January 19–21, 2000.
Andrea Asperti and Stefano Guerrini. The Optimal Implementation of Functional Programming Languages, volume 45 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998.
Nick Benton, Gavin Bierman, Valeria de Paiva, and Martin Hyland. A term calculus for intuitionistic linear logic. TLCA’93, volume 664 of Lecture Notes in Computer Science, pages 75–90, March 1993.
Vincent Danos, Jean-Baptiste Joinet and Harold Schellinx. On the linear decoration of intuitionistic derivations. Archive for Mathematical Logic, 33:387–412, 1995.
Jean-Yves Girard. Light linear logic. Information and Computation, 204:143–175, 1998.
Vinod K. Kathail. Optimal Interpreters for Lambda-calculus Based Functional Programming Languages. PhD thesis, MIT, May 1990.
John Lamping. An Algorithm for Optimal Lambda Calculus Reduction. In ACM POPL’ 90, pages 16–30, New York, NY, USA, 1990.
Jean-Jacques Lévy. Optimal reductions in the lambda-calculus. In Jonathan P. Seldin and J. Roger Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 159–191. Academic Press, London, 1980.
Harry G. Mairson. A simple proof of a theorem of Statman. Theoretical Computer Science, 103(2):387–394, September 1992.
Alberto Pravato and Luca Roversi. Λ! considered both as a paradigmatic language and a meta-language. In Fifth Italian Conference on Theoretical Computer Science, Salerno (Italy), 1995.
Luca Roversi. A Polymorphic Language which Is Typable and Poly-step. In Proc. of the Asian Computing Science Conference (ASIAN’98), volume 1538 of Lecture Notes in Computer Science, pages 43–60, Manila (The Philippines), 1998.
Harold Schellinx. The Noble Art of Linear Decorating. PhD thesis, Institute for Logic, Language and Computation, University of Amsterdam, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coppola, P., Martini, S. (2001). Typing Lambda Terms in Elementary Logic with Linear Constraints. In: Abramsky, S. (eds) Typed Lambda Calculi and Applications. TLCA 2001. Lecture Notes in Computer Science, vol 2044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45413-6_10
Download citation
DOI: https://doi.org/10.1007/3-540-45413-6_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41960-0
Online ISBN: 978-3-540-45413-7
eBook Packages: Springer Book Archive