Advertisement

A Filter Model for the λμ-Calculus

(Extended Abstract)
  • Steffen van Bakel
  • Franco Barbanera
  • Ugo de’Liguoro
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)

Abstract

We introduce an intersection type assignment system for the pure λμ-calculus, which is invariant under subject reduction and expansion. The system is obtained by describing Streicher and Reus’s denotational model of continuations in the category of ω-algebraic lattices via Abramsky’s domain logic approach. This provides a tool for showing the completeness of the type assignment system with respect to the continuation models via a filter model construction. We also show that typed λμ-terms in Parigot’s system have a non-trivial intersection typing in our system.

Keywords

Intersection Type Reduction Rule Natural Deduction Filter Model Type Assignment 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abramsky, S.: Domain Theory in Logical Form. APAL 51, 1–77 (1991)zbMATHGoogle Scholar
  2. 2.
    Alessi, F., Barbanera, F., Dezani-Ciancaglini, M.: Intersection types and lambda models. TCS 355(2), 108–126 (2006)CrossRefzbMATHGoogle Scholar
  3. 3.
    Alessi, F., Severi, P.: Recursive Domain Equations of Filter Models. In: Geffert, V., Karhumäki, J., Bertoni, A., Preneel, B., Návrat, P., Bieliková, M. (eds.) SOFSEM 2008. LNCS, vol. 4910, pp. 124–135. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  4. 4.
    van Bakel, S.: Completeness and Partial Soundness Results for Intersection & Union Typing for \(\overline{\lambda}{\mu}\tilde{\mu}\). APAL 161, 1400–1430 (2010)zbMATHGoogle Scholar
  5. 5.
    van Bakel, S.: Sound and Complete Typing for λμ. In: ITRS 2010. EPTCS, vol. 45, pp. 31–44 (2010)Google Scholar
  6. 6.
    Barbanera, F., Dezani-Ciancaglini, M.: de’Liguoro, U. Intersection and Union Types: Syntax and Semantics. I&C 119(2), 202–230 (1995)Google Scholar
  7. 7.
    Barendregt, H.: The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam (1984)zbMATHGoogle Scholar
  8. 8.
    Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. JSL 48(4), 931–940 (1983)zbMATHGoogle Scholar
  9. 9.
    Bierman, G.M.: A Computational Interpretation of the λμ-calculus. In: Brim, L., Gruska, J., Zlatuška, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 336–345. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  10. 10.
    Coppo, M., Dezani-Ciancaglini, M.: An Extension of the Basic Functionality Theory for the λ-Calculus. NDjFL 21(4), 685–693 (1980)zbMATHGoogle Scholar
  11. 11.
    Curien, P.-L., Herbelin, H.: The Duality of Computation. In: ICFP 2000, ACM Notes 35.9, pp. 233–243 (2000)Google Scholar
  12. 12.
    David, R., Py, W.: λμ-Calculus and Böhm’s Theorem. JSL 66(1), 407–413 (2001)zbMATHGoogle Scholar
  13. 13.
    Dezani-Ciancaglini, M., Honsell, F., Alessi, F.: A complete characterization of complete intersection-type preorders. ACM Trans. Comput. Log. 4(1), 120–147 (2003)CrossRefGoogle Scholar
  14. 14.
    Dougherty, D., Ghilezan, S., Lescanne, P.: Intersection and Union Types in the \(\overline{\lambda}{\mu}\tilde{\mu}\)-calculus. In: ITRS 2004. ENTCS, vol. 136, pp. 228–246 (2004)Google Scholar
  15. 15.
    Dougherty, D., Ghilezan, S., Lescanne, P.: Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage. TCS 398 (2008)Google Scholar
  16. 16.
    Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, p. 68. North Holland, Amsterdam (1969) (1935)Google Scholar
  17. 17.
    Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: Continuous Lattices And Domains. Cambridge University Press, Cambridge (2003)CrossRefzbMATHGoogle Scholar
  18. 18.
    de Groote, P.: On the relation between the λμ-calculus and the syntactic theory of sequential control. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 31–43. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  19. 19.
    Herbelin, H., Saurin, A.: λμ-calculus and Λμ-calculus: a Capital Difference (2010) (manuscript)Google Scholar
  20. 20.
    Hofmann, M., Streicher, T.: Continuation models are universal for λμ-calculus. In: LICS 1997, pp. 387–397 (1997)Google Scholar
  21. 21.
    Hofmann, M., Streicher, T.: Completeness of continuation models for lambda-mu-calculus. I&C 179(2), 332–355 (2002)zbMATHGoogle Scholar
  22. 22.
    Krivine, J.-L.: Lambda calculus, types and models. Ellis Horwood, England (1993)zbMATHGoogle Scholar
  23. 23.
    Lafont, Y., Reus, B., Streicher, T.: Continuation Semantics or Expressing Implication by Negation. Report 9321, Universität München (1993)Google Scholar
  24. 24.
    Meyer, A.R.: What is a Model of the Lambda Calculus? Inf. Contr. 52(1), 87–122 (1982)CrossRefzbMATHGoogle Scholar
  25. 25.
    Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: POPL 1997, pp. 215–227 (1997)Google Scholar
  26. 26.
    Ong, C.-H.L.: A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations. In: LICS 1996, pp. 230–241 (1996)Google Scholar
  27. 27.
    Parigot, M.: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  28. 28.
    Py, W.: Confluence en λμ-calcul. PhD thesis, Universite de Savoie (1998)Google Scholar
  29. 29.
    Saurin, A.: On the relations between the syntactic theories of λμ-calculi. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 154–168. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  30. 30.
    Streicher, T., Reus, B.: Classical logic: Continuation Semantics and Abstract Machines. JFP 11(6), 543–572 (1998)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Steffen van Bakel
    • 1
  • Franco Barbanera
    • 2
  • Ugo de’Liguoro
    • 3
  1. 1.Department of ComputingImperial College LondonLondonUK
  2. 2.Dipartimento di Matematica e InformaticaUniversità degli Studi di CataniaCataniaItalia
  3. 3.Dipartimento di InformaticaUniversità degli Studi di TorinoTorinoItaly

Personalised recommendations