Pure type system

A general framework parameterizing typed lambda calculi by a triple (sorts, axioms, rules), unifying systems like Simply typed lambda calculus, System F, and the Calculus of inductive construction under a single formalism.