×

The \(\lambda_\Delta\)-calculus. (English) Zbl 0942.03512

Hagiya, Masami (ed.) et al., Theoretical aspects of computer software. 2nd international Symposium TACS ’94, Sendai, Japan, April 19-22, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 789, 516-542 (1994).
Summary: By restriction of Felleisen’s control operator \(\mathcal F\) we obtain an operator \(\Delta\) and a fully compatible, Church-Rosser control calculus \(\lambda_\Delta\) enjoying a number of desirable properties. It is shown that \(\lambda_\Delta\) contains a strongly normalizing typed subcalculus with a reduction corresponding closely to systems of proof normalization for classical logic. The calculus is more than strong enough to express a call-by-name catch/throw programming paradigm.
For the entire collection see [Zbl 0925.68012].

MSC:

03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus
PDFBibTeX XMLCite