Comparing Call-by-Name and Call-by-Value Reduction and Reduction Strategies in Calculi for Classical Logic

Steffen van Bakel, David Davies

We define call-by-name and call-by-value reduction and reduction strategies for the calculi slmu (symmetric lmu), lmmt, and Xs (X with implicit substitution). We establish a strong…