New Developments in Environment Machines

In this paper we discuss and compare abstract machines for the lambda-calculus, implementing various evaluation strategies. Starting from the well-known Categorical abstract machine (CAM) and Krivine's abstract machine (KAM), we develop two families of machines that differ in the way they treat environments. The first family is inspired by the work on closed reduction strategies, whereas the second is built in the spirit of the jumping machines based on the work done on Linear Logic.