Type-Theoretic Signatures for Algebraic Theories and Inductive Types

András Kovács

We develop the usage of certain type theories as specification languages for algebraic theories and inductive types. We observe that the expressive power of dependent type theories…