Church’s simple theory of types is pretty much the “basic” type theory; other type theories extend it in various ways. It’s used, e.g., in computer science (some formal proof checkers), linguistics (formal semantics) and philosophy (metaphysics). It can also be used in mathematics as an alternative to the theory of ZFC, which is axiomatized in first-order logic.
I’m not metachirality, but I would recommend any introduction to simple type theory (basically: higher-order logic). If you already know first-order logic, it’s a natural extension. This is a short one: https://www.sciencedirect.com/science/article/pii/S157086830700081X
Church’s simple theory of types is pretty much the “basic” type theory; other type theories extend it in various ways. It’s used, e.g., in computer science (some formal proof checkers), linguistics (formal semantics) and philosophy (metaphysics). It can also be used in mathematics as an alternative to the theory of ZFC, which is axiomatized in first-order logic.