4 ms·
Neither Coq nor Isabelle are based on Martin-Löf Type Theory (in a narrow sense). Coq is based on a variant of the calculus of construction (with (co)inductive
by mafribe 13y ago
Neither Coq nor Isabelle are based on Martin-Löf Type Theory (in a narrow sense).
Coq is based on a variant of the calculus of construction (with (co)inductive definitions) and Isabelle is an LCF-style prover framework that you can instantiate with various different logics. The most widely used variant is Isabelle/HOL which implements a variant of Church's theory of types. To implement other logics, Isabelle uses intuitionistic second order logic based on lambda calculus, without numbers or recursive data types. Idris has Type:Type, so is unsound as a logic. I'm not sure exactly what Epigram uses, but I assume it's somehow based on Luo's ECC. Only Agda is based on Martin-Löf Type Theory.
- tel 13y agoYeah... This is correct as far as I know though a bit out of my complete technical grasp. To my understanding MLTT was a fairly central topic and it helps to distinguish MLTT from just type theory since plain-old-TT might be harder to distinguish as something interesting above `(int *)`. But, to solidify, mafribe is much more correct than my comment and there's, as far as I'm aware, a much larger menagerie of other type theories. The recent Homotopy Type Theory publication—which was on HN as notable due to its publication process—was yet another step in this direction.
- mafribe 13y agoPer Martin-Löf was instrumental in extending type theory to dependent types, although the first version of his dependent type theory was impredicative with Type:Type and was shown to be inconsistent by J.-Y. Girard. Subsequent versions of Martin-Löf type theory have been predicative, but other dependent type theories (such as the calculus of constructions) stuck with (more benign forms of) impredicativity.