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.
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
Abramsky, S.: Domain Theory in Logical Form. APAL 51, 1–77 (1991)
Alessi, F., Barbanera, F., Dezani-Ciancaglini, M.: Intersection types and lambda models. TCS 355(2), 108–126 (2006)
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)
van Bakel, S.: Completeness and Partial Soundness Results for Intersection & Union Typing for \(\overline{\lambda}{\mu}\tilde{\mu}\). APAL 161, 1400–1430 (2010)
van Bakel, S.: Sound and Complete Typing for λμ. In: ITRS 2010. EPTCS, vol. 45, pp. 31–44 (2010)
Barbanera, F., Dezani-Ciancaglini, M.: de’Liguoro, U. Intersection and Union Types: Syntax and Semantics. I&C 119(2), 202–230 (1995)
Barendregt, H.: The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam (1984)
Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. JSL 48(4), 931–940 (1983)
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)
Coppo, M., Dezani-Ciancaglini, M.: An Extension of the Basic Functionality Theory for the λ-Calculus. NDjFL 21(4), 685–693 (1980)
Curien, P.-L., Herbelin, H.: The Duality of Computation. In: ICFP 2000, ACM Notes 35.9, pp. 233–243 (2000)
David, R., Py, W.: λμ-Calculus and Böhm’s Theorem. JSL 66(1), 407–413 (2001)
Dezani-Ciancaglini, M., Honsell, F., Alessi, F.: A complete characterization of complete intersection-type preorders. ACM Trans. Comput. Log. 4(1), 120–147 (2003)
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)
Dougherty, D., Ghilezan, S., Lescanne, P.: Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage. TCS 398 (2008)
Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, p. 68. North Holland, Amsterdam (1969) (1935)
Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: Continuous Lattices And Domains. Cambridge University Press, Cambridge (2003)
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)
Herbelin, H., Saurin, A.: λμ-calculus and Λμ-calculus: a Capital Difference (2010) (manuscript)
Hofmann, M., Streicher, T.: Continuation models are universal for λμ-calculus. In: LICS 1997, pp. 387–397 (1997)
Hofmann, M., Streicher, T.: Completeness of continuation models for lambda-mu-calculus. I&C 179(2), 332–355 (2002)
Krivine, J.-L.: Lambda calculus, types and models. Ellis Horwood, England (1993)
Lafont, Y., Reus, B., Streicher, T.: Continuation Semantics or Expressing Implication by Negation. Report 9321, Universität München (1993)
Meyer, A.R.: What is a Model of the Lambda Calculus? Inf. Contr. 52(1), 87–122 (1982)
Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: POPL 1997, pp. 215–227 (1997)
Ong, C.-H.L.: A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations. In: LICS 1996, pp. 230–241 (1996)
Parigot, M.: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)
Py, W.: Confluence en λμ-calcul. PhD thesis, Universite de Savoie (1998)
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)
Streicher, T., Reus, B.: Classical logic: Continuation Semantics and Abstract Machines. JFP 11(6), 543–572 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Bakel, S., Barbanera, F., de’Liguoro, U. (2011). A Filter Model for the λμ-Calculus. In: Ong, L. (eds) Typed Lambda Calculi and Applications. TLCA 2011. Lecture Notes in Computer Science, vol 6690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21691-6_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-21691-6_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21690-9
Online ISBN: 978-3-642-21691-6
eBook Packages: Computer ScienceComputer Science (R0)