Bidirectional Typechecking (draft)

Bidirectional typechecking is the one typechecking algorithm LVCA has built-in support for. In this post I'd like to cover the basics of what bidirectional typechecking is and how it's supported in LVCA.

What is Bidirectional Typechecking?

In order of increasing formality / length (ie the order you should read them), the best references I know of are: