×

zbMATH — the first resource for mathematics

Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus. (English) Zbl 1018.68016
Summary: This paper proves the confluency and the strong normalizability of the call-by-value \(\lambda \mu\)-calculus with the domain-free style. The confluency of the system is proved by improving the parallel reduction method of Baba et al. The strong normalizability is proved by using the modified CPS-translation, which preserves the typability and the reduction relation. This paper defines the class of the reductions whose strictness is preserved by the modified CPS-translation to prove the strong normalizability.

MSC:
68N18 Functional programming and lambda calculus
Software:
Automath
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baba, K.; Hirokawa, S.; Fujita, K., Parallel reduction in type free \(λμ\)-calculus, Electron. notes theoret. comput. sci., 42, 52-66, (2001) · Zbl 0971.68019
[2] Barbanera, F.; Berardi, S., A strong normalization result for classical logic, Ann. pure appl. logic, 76, 99-116, (1995) · Zbl 0832.03028
[3] Barendregt, H.P., Lambda calculi with types, () · Zbl 0549.03012
[4] David, R.; Py, W., \(λμ\)-calculus and Böhm’s theorem, J. symbolic logic, 66, 1, 407-413, (2001) · Zbl 0981.03019
[5] de Groote, P., A CPS-translation for the \(λμ\)-calculus, (), 85-99 · Zbl 0938.03024
[6] de Groote, P., A simple calculus of exception handling, (), 201-215 · Zbl 1063.68565
[7] Felleisen, M.; Friedman, D.P.; Kohlbecker, E.; Duba, B., A syntactic theory of sequential control, Theoret. comput. sci., 52, 205-237, (1987) · Zbl 0643.03011
[8] Fujita, K., Explicitly typed \(λμ\)-calculus for polymorphism and call-by-value, (), 162-176 · Zbl 0933.03009
[9] Fujita, K., Domain-free \(λμ\)-calculus, Theoret. inform. appl., 34, 433-466, (2000) · Zbl 0974.68032
[10] Girard, J.-Y., The system \(F\) of variable types, fifteen years later, Theoret. comput. sci., 45, 159-192, (1986) · Zbl 0623.03013
[11] Girard, J.-Y.; Taylor, P.; Lafont, Y., Proofs and types, (1989), Cambridge University Press Cambridge
[12] C.-H.L. Ong, C.A. Stewart, A Curry-Howard foundation for functional computation with control, Proc. 24th Annu. ACM Symp. of Principles of Programming Languages, 1997, pp. 215-227.
[13] Parigot, M., \(λμ\)-calculus: an algorithmic interpretation of natural deduction, (), 190-201 · Zbl 0925.03092
[14] Parigot, M., Proofs of strong normalization for second order classical natural deduction, J. symbolic logic, 62, 4, 1461-1479, (1997) · Zbl 0941.03063
[15] Plotkin, G.D., Call-by-name, call-by-value and the \(λ\)-calculus, Theoret. comput. sci., 1, 125-159, (1975) · Zbl 0325.68006
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.