×

zbMATH — the first resource for mathematics

Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage. (English) Zbl 1146.68028
Summary: We develop an intersection type system for the \(\overline{\lambda}\mu\widetilde{\mu}\) calculus of Curien and Herbelin. This calculus provides a symmetric computational interpretation of classical sequent style logic and gives a simple account of call-by-name and call-by-value. The present system improves upon earlier type disciplines for \(\overline{\lambda}\mu\widetilde{\mu}\): in addition to characterizing the \(\overline{\lambda}\mu\widetilde{\mu}\) expressions that are strongly normalizing under free (unrestricted) reduction, the system enjoys the subject reduction and the subject expansion properties.

MSC:
68N18 Functional programming and lambda calculus
03B40 Combinatory logic and lambda calculus
03F05 Cut-elimination and normal-form theorems
Software:
Forsythe
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Barbanera, F.; Berardi, S., A symmetric lambda calculus for classical program extraction, Information and computation, 125, 2, 103-117, (1996) · Zbl 0853.68159
[2] Barbanera, F.; Dezani-Ciancaglini, M.; de’ Liguoro, U., Intersection and union types: syntax and semantics, Information and computation, 119, 2, 202-230, (1995) · Zbl 0832.68065
[3] Barendregt, H.P., The lambda calculus: its syntax and semantics, (1984), North-Holland Amsterdam · Zbl 0551.03007
[4] Barendregt, H.P.; Coppo, M.; Dezani-Ciancaglini, M., A filter lambda model and the completeness of type assignment, Journal of symbolic logic, 48, 4, 931-940, (1984), 1983 · Zbl 0545.03004
[5] Barendregt, H.P.; Ghilezan, S., Lambda terms for natural deduction, sequent calculus and cut-elimination, Journal of functional programming, 10, 1, 121-134, (2000) · Zbl 0949.03055
[6] Boudol, G.; Zimmer, P., On type inference in the intersection type discipline, Electronic notes in theoretical computer science, 136, 23-42, (2005) · Zbl 1272.03073
[7] Buneman, P.; Pierce, B., Union types for semistructured data, (), 184-207 · Zbl 1044.68574
[8] Capitani, B.; Loreti, M.; Venneri, B., Hyperformulae, parallel deductions and intersection types, () · Zbl 1261.03072
[9] Carlier, S.; Wells, J.B., Type inference with expansion variables and intersection types in system E and an exact correspondence with beta-reduction, (), 132-143
[10] Coppo, M.; Dezani-Ciancaglini, M., A new type-assignment for lambda terms, Archiv für mathematische logik, 19, 139-156, (1978) · Zbl 0418.03010
[11] Coppo, M.; Dezani-Ciancaglini, M., An extension of the basic functionality theory for the \(\lambda\)-calculus, Notre dame journal of formal logic, 21, 4, 685-693, (1980) · Zbl 0423.03010
[12] Coppo, M.; Dezani-Ciancaglini, M.; Venneri, B., Principal type schemes and \(\lambda\)-calculus semantics, (), 535-560
[13] Curien, P.-L., Symmetry and interactivity in programming, Bulletin of symbolic logic, 9, 2, 169-180, (2003) · Zbl 1058.03027
[14] Curien, P.-L.; Herbelin, H., The duality of computation, ()
[15] David, R., Normalization without reducibility, Annals of pure and applied logic, 107, 121-130, (2001) · Zbl 0966.03015
[16] David, R.; Nour, K., Arithmetical proofs of strong normalization results for the symmetric \(\lambda \mu\)-calculus, (), 162-178 · Zbl 1112.03309
[17] David, R.; Nour, K., Why the usual candidates of reducibility do not work for the symmetric \(\lambda \mu\)-calculus, Electronic notes in theoretical computer science, 140, 101-111, (2005) · Zbl 1272.68082
[18] Dezani-Ciancaglini, M.; Ghilezan, S.; Venneri, B., The “relevance” of intersection and union types, Notre dame journal of formal logic, 38, 2, 246-269, (1997) · Zbl 0918.03008
[19] Dougherty, D.; Ghilezan, S.; Lescanne, P., Characterizing strong normalization in a language with control operators, (), 155-166
[20] Dougherty, D.; Ghilezan, S.; Lescanne, P., Intersection and union types in the \(\overline{\lambda} \mu \widetilde{\mu}\)-calculus, (), 153-172 · Zbl 1272.03078
[21] Dougherty, D.; Ghilezan, S.; Lescanne, P.; Likavec, S., Strong normalization of the dual classical sequent calculus, (), 169-183 · Zbl 1143.03360
[22] Dunfield, J.; Pfenning, F., Type assignment for intersections and unions in call-by-value languages, (), 250-266 · Zbl 1029.68098
[23] Dunfield, J.; Pfenning, F., Tridirectional typechecking, (), 281-292 · Zbl 1325.68062
[24] Griffin, T., A formulae-as-types notion of control, (), 47-58
[25] H. Herbelin, Personal communication
[26] H. Herbelin, Séquents qu’on calcule : de l’interprétation du calcul des séquents comme calcul de \(\lambda\)-termes et comme calcul de stratégies gagnantes. Thèse d’université, Université Paris 7, Janvier 1995
[27] H. Herbelin, C’est maintenant qu’on calcule, au cœur de la dualité. Mémoire d’habiliation, Université de Paris-Orsay, December 2005
[28] Hindley, J.R., Coppo – dezani types do not correspond to propositional logic, Theoretical computer science, 28, 1-2, 235-236, (1984) · Zbl 0529.03003
[29] Knaster, B., Un théorème sur LES fonctions d’ensembles, Annales de la societé polonaise de mathematique, 6, 133-134, (1928) · JFM 54.0091.04
[30] Lengrand, S., Call-by-value, call-by-name, and strong normalization for the classical sequent calculus, () · Zbl 1270.68070
[31] S. Likavec, Types for object oriented and functional programming languages, Ph.D. Thesis, Università di Torino, Italy and ENS Lyon, France, 2005
[32] Palsberg, J.; Pavlopoulou, C., From polyvariant flow information to intersection and union types, Journal of functional programming, 11, 3, 263-317, (2001) · Zbl 0976.68024
[33] Parigot, M., An algorithmic interpretation of classical natural deduction, (), 190-201 · Zbl 0925.03092
[34] B.C. Pierce, Programming with intersection types, union types, and polymorphism, Technical Report CMU-CS-91-106, Carnegie Mellon University, February 1991
[35] Polonovski, E., Strong normalization of \(\lambda \mu \widetilde{\mu}\)-calculus with explicit substitutions, (), 423-437 · Zbl 1126.03307
[36] Pottinger, G., Normalization as homomorphic image of cut-elimination, Annals of mathematical logic, 12, 323-357, (1977) · Zbl 0378.02017
[37] Pottinger, G., A type assignment for the strongly normalizable \(\lambda\)-terms, (), 561-577
[38] J.C. Reynolds, Design of the programming language Forsythe, Report CMU-CS-96-146, Carnegie Mellon University, Pittsburgh, PA, June 28, 1996
[39] Ronchi Della Rocca, S.; Roversi, L., Intersection logic, (), 421-428 · Zbl 0999.03011
[40] Sallé, P., Une extension de la théorie des types en lambda-calcul, (), 398-410
[41] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific journal of mathematics, 5, 285-309, (1955) · Zbl 0064.26004
[42] Urban, C.; Bierman, G.M., Strong normalisation of cut-elimination in classical logic, (), 365-380 · Zbl 0934.03074
[43] van Bakel, S., Principal type schemes for the strict type assignment system, Logic and computation, 3, 6, 643-670, (1993) · Zbl 0802.68024
[44] van Bakel, S., Intersection type assignment systems, Theoretical computer science, 38, 2, 246-269, (1997)
[45] Ph. Wadler, Call-by-value is dual to call-by-name, in: Proc. of the 8th Int. Conference on Functional Programming, 2003, pp. 189-201 · Zbl 1315.68060
[46] Wadler, Ph., Call-by-value is dual to call-by-name, reloaded, (), 185-203 · Zbl 1078.68020
[47] Wells, J.B.; Dimock, A.; Muller, R.; Turbak, F., A calculus with polymorphic and polyvariant flow types, Journal of functional programming, 12, 3, 183-227, (2002) · Zbl 1005.68042
[48] Wells, J.B.; Haack, C., Branching types, (), 115-132 · Zbl 1077.68568
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.