Nuprl

H. Schwichtenberg and R. Steinbruggen (eds.), Proof and System-Reliability: 213-259. The Nuprl Book: "Introduction to Type Theory. （页面存档备份，存于互联网档案馆）"

{\displaystyle \alpha } 不能用在 α {\displaystyle \alpha } 被实例化为一个多态类形。直谓类型理论包括直觉类型论与NuPRL（英语：Nuprl） 非直谓多态（Impredicative polymorphism），也称“头等多态”（first-class

是目前对这种折中是否是不可避免的和在内涵类型论中缺乏外延原理是一个特色还是一个缺陷的讨论的一个主题。 类型论已经被用做很多证明助理的基础，比如 NuPRL、LEGO、Coq 和 Agda。最近，依赖类型也作为编程语言设计的特征，比如Dependent ML 和 Epigram。 直觉主义 BHK释义

马丁-洛夫开创的直觉类型论提出了依赖类型的概念，直接启发了构造演算（CoC）与LF逻辑框架的建立。一些流行的计算机证明系统和程序语言在此基础上得以开发，包括：Coq、Agda、NuPRL、LEGO、Twelf 和 Epigram等。 佩尔·马丁-洛夫是瑞典皇家科学院以及欧洲科学院（Academia Europaea）的院士。 See

是 是（可选） 任意项 是 否 是 是 Matita（英语：Matita） 是 纯函数式 是 是 是 任意项 是 是 OCaml 是 Nuprl（英语：Nuprl） 是 纯函数式 是 是 是 任意项 是 ? 是 ? F* 是 函数式 / 命令式 ? ? ? ? ? ? ? ? PVS（英语：Prototype