This paper describes optimizations for checking proofs represented in
the Edinburgh Logical Framework (LF).  The optimizations allow large
proofs to be checked efficiently which cannot feasibly be checked
using the standard algorithm for LF.  The crucial optimization is a
form of result caching.  To formalize this optimization, a path
calculus for LF is developed and shown equivalent to a standard
calculus.