Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
martin-loef_type_theory [2014/11/10 18:08] nikolaj created |
martin-loef_type_theory [2015/04/01 10:37] nikolaj |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ===== Martin-Löf type theory ===== | ===== Martin-Löf type theory ===== | ||
| - | ==== Meta ==== | + | ==== Framework ==== |
| - | >todo | + | A [[Dependent type theory]] with [[Identity type]]. Or rather it's an umbrella term for several closely related such theories. |
| - | ==== Discussion ==== | + | |
| - | >todo | + | ----- |
| === Reference === | === Reference === | ||
| - | >todo | + | Wikipedia: [[http://en.wikipedia.org/wiki/Intuitionistic_type_theory|Intuitionistic type theory]] |
| - | ==== Parents ==== | + | |
| - | === Related === | + | ----- |
| - | [[Dependent type theory]] | + | === Requirements === |
| + | [[Identity type]] | ||
