used by Twelf, often to define other type theories;
* many type theories which fall under higher-order logic are used by the HOL family of provers and PVS;
* computational type theory is used by NuPRL;
* calculus of constructions and its derivatives are used by Rocq