An abstract property of confluence applied to the study of the lazy partial lambda calculus

Abstract:

The partial λ-calculus, introduced by E. Moggi, is a formalism well adapted to study the logic of programs in which the evaluation mechanism is call-by-value. In this paper we consider a lazy version of the partial λ-calculus. The main result is the Church-Rosser property for the class of strongly normalizable terms. First, we find sufficient conditions for confluence in an abstract framework. Then, we prove that our calculus satisfies those conditions.

Año de publicación:

1994

Keywords:

Fuente:

scopus