Abstract
System \(\mathcal{L}\) is a linear λ-calculus with numbers and an iterator, which, although imposing linearity restrictions on terms, has all the computational power of Gödel’s System \(\mathcal{T}\). System \(\mathcal{L}\) owes its power to two features: the use of a closed reduction strategy (which permits the construction of an iterator on an open function, but only iterates the function after it becomes closed), and the use of a liberal typing rule for iterators based on iterative types. In this paper, we study these new types, and show how they relate to intersection types. We also give a sound and complete type reconstruction algorithm for System \(\mathcal{L}\).
Research partially supported by the British Council Treaty of Windsor Grant: “Linearity: Programming Languages and Implementations”, and by funds granted to LIACC through the Programa de Financiamento Plurianual, Fundação para a Ciência e Tecnologia and FEDER/POSI.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abramsky, S.: Computational Interpretations of Linear Logic. Theoretical Computer Science 111, 3–57 (1993)
Alves, S.: The power of closed-reduction strategies. In: Proceedings of WRS 2006, 6th International Workshop on Rewriting Strategies, FLOC 2006, Seattle (2006)
Alves, S., et al.: The power of linear functions. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, Springer, Heidelberg (2006)
Bakel, S.: Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Department of Computer Science, University of Nijmegen (1993)
Bakel, S.: Intersection type assignment systems. Theoretical Computer Science 151(2), 385–435 (1995)
Barendregt, H.P., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type-assignment. J. Symbolic Logic 48, 931–940 (1983)
Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic 21(4), 685–693 (1980)
Damas, L.M.M.: Type Assignment in Programming Languages. PhD thesis, University of Edinburgh (1985)
Damas, L.M.M., Milner, R.: Principal type schemes for functional programs. In: Conference Record of the Ninth Annual ACM Symposium on the Principles of Programming Languages, pp. 207–212. ACM Press, New York (1982)
Damiani, F.: Rank-2 intersection and polymorphic recursion (2005)
Fernández, M., Mackie, I., Sinot, F.-R.: Closed reduction: explicit substitutions without alpha conversion. Mathematical Structures in Computer Science 15(2), 343–381 (2005)
Girard, J.-Y.: Linear Logic. Theoretical Computer Science 50(1), 1–102 (1987)
Girard, J.-Y.: Geometry of interaction 1: Interpretation of System F. In: Ferro, R., et al. (eds.) Logic Colloquium 88. Studies in Logic and the Foundations of Mathematics, vol. 127, pp. 221–260. North Holland, Amsterdam (1989)
Girard, J.-Y.: Towards a geometry of interaction. In: Gray, J.W., Scedrov, A. (eds.) Categories in Computer Science and Logic: Proc. of the Joint Summer Research Conference, pp. 69–108. American Mathematical Society, Providence (1989)
Haack, C., Wells, J.B.: Type error slicing in implicitly typed higher-order languages. Sci. Comput. Program. 50(1-3), 189–224 (2004), doi:10.1016/j.scico.2004.01.004
Jim, T.: Rank 2 type systems and recursive definitions. Technical report, Massachusetts Institute of Technology (1995)
Jim, T.: What are principal typings and what are they good for? In: Proceedings of the 23rd ACM Symposium on Principles of Programming Languages (POPL’96), ACM Press, New York (1996)
Kfoury, A.J., et al.: Relating typability and expressibility in finite-rank intersection type systems. In: Proceedings of the 1999 International Conference on Functional Programming, pp. 90–101. ACM Press, New York (1999)
Lafont, Y.: Interaction nets. In: Proceedings of the 17th ACM Symposium on Principles of Programming Languages (POPL’90), Jan. 1990, pp. 95–108. ACM Press, New York (1990)
Mackie, I.: Lilac: A functional programming language based on linear logic. Journal of Functional Programming 4(4), 395–433 (1994)
Martelli, A., Montanari, U.: An efficient unification algorithm. Transactions on Programming Languages and Systems 4(2), 258–282 (1982)
Milner, R.: A theory of type polymorphism in programming. Journal of Computer and System Sciences 17(3), 348–375 (1978)
Pottinger, G.: A type assignment for strongly normalizable λ-terms. In: To H.B. Curry, Essays in Combinatory Logic, Lambda-Calculus and Formalism, pp. 535–560. Academic Press, London (1980)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12(1), 23–41 (1965)
Toyama, Y.: Confluent term rewriting systems with membership. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol. 308, pp. 228–241. Springer, Heidelberg (1988)
Yamada, J.: Confluence of terminating membership conditional trs. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol. 656, pp. 378–392. Springer, Heidelberg (1993)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Alves, S., Fernández, M., Florido, M., Mackie, I. (2007). Iterator Types. In: Seidl, H. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2007. Lecture Notes in Computer Science, vol 4423. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71389-0_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-71389-0_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71388-3
Online ISBN: 978-3-540-71389-0
eBook Packages: Computer ScienceComputer Science (R0)