DISI, Università di Genova,
Dipartimento di Informatica e Scienze dell'Informazione,
Via Dodecaneso 35, 16146 Genova, Italy;
2 Università di Torino, Dipartimento di Informatica, C.so Svizzera 185, 10149 Torino, Italy; firstname.lastname@example.org.
Accepted: August 1999
The notion of solvability in the call-by-value λ-calculus is defined and completely characterized, both from an operational and a logical point of view. The operational characterization is given through a reduction machine, performing the classical β-reduction, according to an innermost strategy. In fact, it turns out that the call-by-value reduction rule is too weak for capturing the solvability property of terms. The logical characterization is given through an intersection type assignment system, assigning types of a given shape to all and only the call-by-value solvable terms.
Mathematics Subject Classification: 68Q05 / 03D10
Key words: Models of computations / λ-calculus / call-by-value.
© EDP Sciences, 1999