How to prove type soundness of Java-like languages without forgoing big-step semantics
Davide Ancona · 2014
Small-step operational semantics is the most commonly employed formalism for proving type soundness of statically typed programming languages, because of its ability to distinguish stuck from non-terminating computations, as opposed to big-step operational semantics.