This document comprises an example of typechecking a type system based on System F, in a small ML-like language.
You can skip the below section if you already understand System F itself.
System F is the name given to an extension of the simply typed lambda calclus.