Hey, started a repo for tracking type theory history: github.com/prathyvsh/hist I am looking for some resources that would help me catalogue it close to what I’ve done here: github.com/prathyvsh/nota Would you happen to know any resources that would aid me towards this?
Conversation
Replying to
Slightly tangential, but I'd love to find a reference for how type theory and types in PL developed independently, then were eventually combined later on:
Quote Tweet
History subtweet: I regularly see the claim that "type theory invented type systems": that we have static typing because people tried to apply type theory to programming. This is untrue. The two concepts developed independently and were unified much later.
Show this thread
1
3
This might be useful too? It's more about the current state of affairs though, than the history:
Quote Tweet
“What are we thinking when we present a type theory?” by Peter LeFanu Lumsdaine: youtube.com/watch?v=kQe0kn
I found the clarification of some of the hidden rules you have in your head when reading type theories really interesting and worthwhile!
Show this thread
2
1
Show replies


