Abstract
We characterize those terms which are strongly normalizing in a composition-free calculus of explicit substitutions by defining a suitable type system using intersection types. The key idea is the notion of available variable in a term, which is a generalization of the classical notion of free variable.
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Cardelli, L., Curien, P.-L., and Lévy, J.-J. (1991). Explicit substitutions. Journal of Functional Programming, 1 (4): 375–416.
Barendregt, H. P. (1984). The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics. Elsevier Science Publishers B. V. ( North-Holland), Amsterdam. Second edition.
Benaissa, Z., Briaud, D., Lescanne, P., and Rouyer-Degli, J. (1996). Av, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming, 6 (5): 699–722.
Bloo, R. and Geuvers, J. H. (1999). Explicit substitution: on the edge of strong normalization. Theoretical Computer Science, 211: 375–395.
Bloo, R. and Rose, K. H. (1995). Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In CSN ’85—Computing Science in the Netherlands, pages 62–72, Koninklijke Jaarbeurs, Utrecht.
Bucciarelli, A., Lorenzis, S. D., Piperno, A., and Salvo, I. (1999). Some computational properties of intersection types. In 14th Symposium on Logic in Computer Science (LICS’99),pages 109–118, Washington — Brussels — Tokyo. IEEE.
Cardone, F. and Coppo, M. (1990). Two extension of Curry2019s type inference system. In Odifreddi, P., editor, Logic and Computer Science, volume 31 of APIC Series, pages 19–75. Academic Press, New York, NY.
Curien, P.-L., Hardin, T., and Lévy, J.-J. (1996). Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43 (2): 362–397.
Davies, R. and Pfenning, F. (2000). Intersection types and computational effects. In Proceedings of the ACM Sigplan International Conference on Functional Programming (ICFP-00), volume 35.9 of ACM Sigplan Notices, pages 198–208, N.Y. ACM Press.
Dezani-Ciancaglini, M., Honsell, F., and Motohama, Y. (2000). Compositional characterization of lambda -terms using intersection types. In Mathematical Foundation of Computer Science,volume 1893 of Lecture Notes in Computer Science,pages 304–314. Springer-Verlag. extended abstract.
Dougherty, D. and Lescanne, P. (2001). Reductions, intersection types, and explicit substitutions (extended abstract). In Abramsky, S., editor, TLCA 2001–5th Int. Conf. on Typed Lambda Calculus and Applications, volume 2044 of Lecture Notes in Computer Science, pages 121–135, Krakow, Poland. Springer-Verlag.
Dougherty, D. and Lescanne, P. (to appear). Reductions, intersection types, and explicit substitutions. Mathematical Structures in Computer Science.
Ghilezan, S. (2001). Full intersection types and topologies in lambda calculus. JCSS: Journal of Computer and System Sciences, 62 (1): 1–14.
Kamareddine, F. and Ríos, A. (1997). Extending a lambda-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms. Journal of Functional Programming, 7 (4): 395–420.
Kfoury, A. J. and Wells, J. B. (1999). Principality and decidable type inference for finite-rank intersection types. In ACM, editor, POPL ’99. Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of programming languages, January 2022, 1999, San Antonio, TX, ACM SIGPLAN Notices, pages 161–174, New York, NY, USA. ACM Press.
Krivine, J.-L. (1993). Lambda calculus, types and models. Ellis Horwood.
Lescanne, P. (1994). Fromλσ to λυ: a journey through calculi of explicit substitutions. In Boehm, H.-J., editor, POPL ’94–21st Annual ACM Symposium on Principles of Programming Languages, pages 60–69, Portland, Oregon. ACM.
Melliès, P.-A. (1995). Typed λ-calculi with explicit substitution may not terminate. In Dezani, M., editor, TLCA ’95—Int. Conf. on Typed Lambda Calculus and Applications, volume 902 of Lecture Notes in Computer Science, pages 328–334, Edinburgh, Scotland. Springer-Verlag.
Ritter, E. (1999). Characterising explicit substitutions which preserve termination. In TLCA’99, Int. Conf. on Typed Lambda Calculus and Applications,volume 1581 of Lecture Notes in Computer Science,pages 325–339. Springer-Verlag.
Rose, K. (1996). Operational Reduction Models for Functional Programming Languages. PhD thesis, DIKU, Universitetsparken 1, DK-2100 København Ø. DIKU report 96/1.
van Bakel, S. and Dezani-Ciancaglini, M. (2002). Characterizing strong normalization for explicit substitutions. In Latin American Theoretical INformatics — LATIN. to appear.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer Science+Business Media New York
About this chapter
Cite this chapter
Dougherty, D., Lengrand, S., Lescanne, P. (2002). An Improved System of Intersection Types for Explicit Substitutions. In: Baeza-Yates, R., Montanari, U., Santoro, N. (eds) Foundations of Information Technology in the Era of Network and Mobile Computing. IFIP — The International Federation for Information Processing, vol 96. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35608-2_42
Download citation
DOI: https://doi.org/10.1007/978-0-387-35608-2_42
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5275-5
Online ISBN: 978-0-387-35608-2
eBook Packages: Springer Book Archive