The sequent calculus proof system, as an alternative to natural deduction and Hilbert-style systems, has been well-appreciated for its structural symmetry and its applicability to automated proof search. Over the past decade, it has additionally been shown to have a computational significance, perhaps most notably as a type system for the X-calculus, designed by Hugo Herbelin. It is the purpose of this thesis to demonstrate that the structural properties of the X-calculus (derived from the underlying type system) are ideally suited for describing the states and transitions of several abstract machines that have been developed for executing programs written in a functional style. We explore the surrounding issues and offer formal translations of several abstract machines into versions of the X-calculus. In particular, we consider the Krivine machine, the SECD machine, and the ZINC abstract machine.