# Tag Info

### Why colon to denote that a value belongs to a type?

The main reason to prefer the colon notation $t : T$ to the membership relation $t \in T$ is that the membership relation can be misleading because types are not (just) collections. [Supplemental: I ...
• 27.5k

### What's the relation and difference between Calculus of Inductive Constructions and Intuitionistic Type Theory?

I've already answered somewhat, but I'll try to give a more detailed overview of the type theoretical horizon, if you will. I'm a bit fuzzy on the historical specifics, so more informed readers will ...
• 13.4k
Accepted

Accepted

• 27.5k
Accepted

### What kind of theoretical object corresponds to a C++ concept?

From a programming language theory perspective, as opposed to the computability perspective other answers and comments have offered, C++ templates combined with concepts correspond to bounded ...
• 16.6k
Accepted

### Applications of algebraic geometry in type theory/programming language theory

To my knowledge (which is definitely incomplete), there has been relatively little work on this, presumably because it requires assimilating two relatively intricate bodies of knowledge. However, ...
• 32.1k