Abstract
The \(\overline{\lambda}\mu\widetilde{\mu}\)-calculus, defined by Curien and Herbelin [7], is a variant of the λμ-calculus that exhibits symmetries such as term/context and call-by-name/call-by-value. Since it is a symmetric, and hence a non-deterministic calculus, usual proof techniques of normalization needs some adjustments to be made to work in this setting. Here we prove the strong normalization (SN) of simply typed \(\overline{\lambda}\mu\widetilde{\mu}\)-calculus with explicit substitutions. For that purpose, we first prove SN of simply typed \(\overline{\lambda}\mu\widetilde{\mu}\)-calculus (by a variant of the reducibility technique from Barbanera and Berardi [2]), then we formalize a proof technique of SN via PSN (preservation of strong normalization), and we prove PSN by the perpetuality technique, as formalized by Bonelli [5].
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit Substitutions. Journal of Functional Programming (1991)
Barbanera, F., Berardi, S.: A symmetric lambda-calculus for classical program extraction. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 495–515. Springer, Heidelberg (1994)
Benaissa, Z.-E.-A., Briaud, D., Lescanne, P., Rouyer-Degli, J.: λυ, a calculus of explicit substitutions which preserves strong normalisation. Journal of Functional Programming (1996)
Bloo, R., Geuvers, H.: Explicit Substitution: on the Edge of Strong Normalisation. Theoretical Computer Science 211, 375–395 (1999)
Bonelli, E.: Substitutions explicites et réécriture de termes. PhD thesis, Université Paris XI Orsay (2001)
Church, A.: The Calculi of Lambda Conversion. Princeton Univ. Press, Princeton (1941)
Curien, P.-L., Herbelin, H.: The duality of computation. In: Proceedings of ICFP 2000, pp. 233–243. ACM Press, New York (2000)
Guillaume, B.: Un calcul de substitution avec étiquettes. PhD thesis, Université de Savoie (1999)
Herbelin, H.: Explicit substitutions and reducibility. Journal of Logic and Computation 11, 429–449 (2001)
Mellies, P.-A.: Typed λ-calculi with explicit substitutions not terminate. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 328–334. Springer, Heidelberg (1995)
Parigot, M.: λμ-calculus: An algorithmic interpretation of classical natural deduction. In: Proceedings of LICS 1993, pp. 39–46. Computer Society Press (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Polonovski, E. (2004). Strong Normalization of \(\overline{\lambda}\mu\widetilde{\mu}\)-Calculus with Explicit Substitutions. In: Walukiewicz, I. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2004. Lecture Notes in Computer Science, vol 2987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24727-2_30
Download citation
DOI: https://doi.org/10.1007/978-3-540-24727-2_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21298-0
Online ISBN: 978-3-540-24727-2
eBook Packages: Springer Book Archive