# Tag Info

## Hot answers tagged type-theory

### 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 ...
• 26.8k
Accepted

### What are some good introductory books on type theory?

Software Foundations by Benjamin C. Pierce would be a good place to start. It would be a make a good precursor to his Types and Programming Languages. There is also Simon Thompson's Type Theory and ...
• 574

### 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.3k
Accepted

### Why was there a need for Martin-Löf to create intuitionistic type theory?

Very briefly: the simply-typed $\lambda$-calculus does not have dependent types. Dependent types were proposed by de Bruijn and Howard who wanted to extend the Curry-Howard correspondence from ...
• 10.4k
Accepted

• 26.8k
Accepted

### Why is regularity a problem in cubical type theory?

The difficulty is in making such a reduction compatible with all the other reductions involving transport/coe. From one perspective it is a “confluence” problem. It is unfortunate that in the ...
Accepted

### Which universities in the U.S. are doing research in type theory?

Any such list is always subjective, but the best approach to answer this question is: Look at journals/conferences in the area you're interested in. For type theory, I'd look at LICS, LMCS, POPL, ...
• 2,724
Accepted

### Can affine lambda calculus solve every problem in P?

Edit: my guess in the first paragraph below is wrong! Ugo Dal Lago pointed out to me a later paper by Martin Hofmann (appeared in POPL 2002), of which I was unaware, showing (as a corollary of more ...
• 4,823