type-theory.md

Type Theory

Luca Cardelli's paper on Type Systems¹ provides a good introduction to type theory and it's notation. Whilst we normally define a language's syntax with EBNF or similar methods, vary rarely does a language include formalisms for the type system. I would like to be able to provide documentation as well.

We can typeset the notation with $\LaTeX$ within the markdown files as follows:

$$\Gamma \vdash \mathfrak J$$
$$\varnothing, x : Nat \vdash x+1 : Nat$$
$$\Gamma \vdash \diamond$$

In Markdown Preview (VSCode), renders as:

$$\Gamma \vdash \mathfrak J$$ $$\varnothing, x \colon Nat \vdash x+1 \colon Nat$$ $$\Gamma \vdash \diamond$$

On Github:

References

[1] Luca Cardelli, 2004. Type Systems. CRC Handbook of Computer Science and Engineering, 2nd Edition, Ch. 97.