New answers tagged pl.programming-languages
0
I think that you've asked two slightly different questions which are both worth answering. Other answers are good for the question in the title, but I want to focus on the word "fundamental" in your second question.
For large fragments of most mainstream programming languages, there exists a native type theory (discussed at nCafé: 1 2 3) which ...
4
To me, type theory bridges programming with models and proof theories. In particular, I can use category theory to think about programming languages when the underlying type theory has a categorical model (e.g. the intuitionistic type theory by Martin Löf).
On the other hand, type theory to programming is like (point-set) topology to analysis -- it gives you ...
3
"Types are the leaven of computer programming; they make it digestible." Robin Milner
Top 50 recent answers are included
