  The theory of the call-by-value lambda-calculus relies on weak evaluation and
closed terms, that are natural hypotheses in the study of programming
languages. To model proof assistants, however, strong evaluation and open terms
are required. Open call-by-value is the intermediate setting of weak evaluation
with open terms, on top of which Gr\'egoire and Leroy designed the abstract
machine of Coq. This paper provides a theory of abstract machines for open
call-by-value. The literature contains machines that are either simple but
inefficient, as they have an exponential overhead, or efficient but heavy, as
they rely on a labelling of environments and a technical optimization. We
introduce a machine that is simple and efficient: it does not use labels and it
implements open call-by-value within a bilinear overhead. Moreover, we provide
a new fine understanding of how different optimizations impact on the
complexity of the overhead.
