New answers tagged


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 ...


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 ...


"Types are the leaven of computer programming; they make it digestible." Robin Milner

Top 50 recent answers are included