直観主義型理論
マルティン=レーフは、この型理論を数学における構成主義の原理に基づいて設計をおこなった。構成主義は、「証拠」を含んだ存在証明を必要とする。すなわち、「1000より大きい素数が存在する」という証明においては、1000よりも大きくかつ素数である特定の数を確定しなければならない。直観主義型理論は、BHK解釈(Brouwer–Heyting–Kolmogorov interpretation)を内部化するという設計方針を達成している。興味深い点として、証明(proof)が、調査、比較、そして操作できる数学的対象になるというところがある。
直観主義型理論の型構築子(type constructor)は、論理演算子(logical connective)と一対一で対応するように作られている。例えば、含意と呼ばれる論理演算子( A ⟹ B {\displaystyle A\implies B} )は、関数型( A → B {\displaystyle A\to B} )に対応する。この対応はカリー=ハワード同型対応と呼ばれる。かつての型理論もこの同型対応に従っていたが、現在のマルティン=レーフの型理論は依存型(dependent type)を導入することによって述語論理をそのように拡張した最初のものである。