Abstract
By restriction of Felleisen’s control operator F we obtain an operator A and a fully compatible, Church-Rosser control calculus λΔ, enjoying a number of desirable properties. It is shown that λΔ 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.
Cite
CITATION STYLE
Rehof, N. J., & Sørensen, M. H. (1994). The λΔ-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 789 LNCS, pp. 516–542). Springer Verlag. https://doi.org/10.1007/3-540-57887-0_113
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
