I wrote a little post about the typechecking algorithm I devised for SaberVM, a typed stack-based bytecode language like Web Assembly, designed from the ground up for being the target of functional programming languages. Typechecking stack-based bytecode is extremely pretty and elegant, and not talked about very much!