Hostname: page-component-6bf8c574d5-8gtf8 Total loading time: 0 Render date: 2025-02-22T01:50:57.307Z Has data issue: false hasContentIssue false
  • English
  • Français

The approximation theorem for the Λμ-calculus

Published online by Cambridge University Press:  28 July 2015

UGO DE'LIGUORO
UGO DE'LIGUORO*
Affiliation:
Dipartimento di Informatica, Università di Torino, c.so Svizzera 185, 10149 Torino, Italy Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We consider a notion of approximation for terms of de Groote–Saurin Λμ-calculus. Then, we introduce an intersection type assignment system for that calculus which is invariant under subject conversion. The type assignment system also induces a filter model, which is an extensional Λμ-model in the sense of Nakazawa and Katsumata. We then establish the approximation theorem, stating that a type can be assigned to a term in the system if and only if it can be assigned to same of its approximations.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 27 , Special Issue 5: Computing with Lambda-terms. A Special Issue Dedicated to Corrado Böhm for his 90th Birthday , June 2017 , pp. 560 - 580
Copyright
Copyright © Cambridge University Press 2015 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abramsky, S. (1991). Domain theory in logical form. Annals of Pure and Applied Logic 51 (1–2) 1–77.Google Scholar
Barendregt, H. P. (1984). The Lambda Calculus – Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics volume 103, North-Holland.Google Scholar
Barendregt, H. P., Coppo, M. and Dezani-Ciancaglini, M. (1983). A filter lambda model and the completeness of type assignment. Journal Symbolic Logic 48 (4) 931–940.Google Scholar
David, R. and Walter, P.. (2001). λμ-calculus and Böhm's theorem. Journal Symbolic Logic 66 (1) 407–413.Google Scholar
Dezani-Ciancaglini, M., Honsell, F. and Motohama, Y. (2001). Approximation theorems for intersection type systems. Journal of Logicand Computation 11 (3) 395–417.CrossRefGoogle Scholar
de Groote, P. (1994a). A CPS-translation of the Lambda-μ-calculus. In: CAAP. Lecture Notes in Computer Science 787 85–99.CrossRefGoogle Scholar
de Groote, P. (1994b). On the relation between the lambda-mu-calculus and the syntactic theory of sequential control. In: LPAR. Springer Lecture Notes in Computer Science 31–43.CrossRefGoogle Scholar
Herbelin, H. and Ghilezan, S. (2008). An approach to call-by-name delimited continuations. In: Proceedings of POPL'08 383–394.Google Scholar
Nakazawa, K. and Katsumata, S. (2012). Extensional models of untyped Λ-μ calculus. In: Proceedings of Fourth Workshop on Classical Logic and Computation (CL&C'12). Electronic Proceedings in Theoretical Computer Science, 97 35–47.Google Scholar
Parigot, M. (1992). An algorithmic interpretation of classical natural deduction. In: Proceedings of 3rd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'92). Springer Lecture Notes in Computer Science 624 190–201.CrossRefGoogle Scholar
Py, W. (1998). Confluence en λμ-calcul, Ph.D. thesis, Universite de Savoie.Google Scholar
Saurin, A. (2005). Separation with streams in the λμ-calculus. In: Proceedings of LICS'05 356–365.Google Scholar
Saurin, A. (2008a). Une étude logique du contrôle (appliquée à la programmation fonctionnelle et logique). PhD thesis, École Polytechnique.Google Scholar
Saurin, A. (2008b). On the relations between the syntactic theories of λμ-calculi. In: CSL. Lecture Notes in Computer Science 5213 154–168.Google Scholar
Saurin, A. (2010a). Standardization and Böhm trees for λμ calculus. In: Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19–21, 2010. Proceedings. Lecture Notes in Computer Science 6009 134–149.Google Scholar
Saurin, A. (2010b). A Hierarchy for delimited continuations in call-by-name. In: Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Paphos, Cyprus, March 20–28, 2010. Proceedings. Lecture Notes in Computer Science 6014 374–388.Google Scholar
Saurin, A. (2010c). Typing streams in the λμ-calculus. ACM Transactions on Computational Logic, 11 (4).Google Scholar
Saurin, A. (2012). Böhm theorem and Böhm trees for the λμ-calculus. Theoretical Computer Science 435 106–138.Google Scholar
Streicher, T. and Reus, B. (1998). Classical logic, continuation semantics and abstract machines. Journalof Functional Programming, 8 (6) 543–572.Google Scholar
van Bakel, S., Barbanera, F. and de'Liguoro, U. (2011). A filter model for λμ. In: Luke, O. (ed.) Proceedings of TLCA'11. ARCoSS/Lecture Notes in Computer Science 6690 213–228.Google Scholar
van Bakel, S., Barbanera, F. and de'Liguoro, U. (2013) Characterisation of strongly normalising λμ-terms. In: Post Proceedings of ITRS'12. Electronic Proceedings in Theoretical Computer Science. To appear.CrossRefGoogle Scholar