The Java Virtual Machine (JVM) is used extensively in computing environments in which security is a primary concern. The proper formalization of the JVM provides a basis for judgements about the security of JVM programs. Sequent calculi can provide a formalization that allows a shallow encoding of JVM structures into the calculus. This should allow the construction of code verification systems with a smaller trusted code base than the current proof-carrying code technology. This document shows an encoding in Curien and Herbelin calculus, and presents an algorithm for establishing the type-safety of translated programs. Our approach allows a more expressive verification process than traditional methods.