Typechecking

The development proceeds through three layers:

BasicConcepts: types, literals, schemes, and contexts.

Unification: substitution, free variables, and most general unifiers.

AlgorithmW: instantiation, generalization, typing rules, and inference soundness.

Start with Basic concepts, then Unification, and finally Algorithm W. The executable unification and inference procedures are still to be implemented.