Idris

2022年9月25日 (日) 16:50的最后版本

您可以在Wikipedia上了解到此条目的英文信息 Idris Thanks, Wikipedia.

Idris programming language

[编辑] 简介

Idris 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。

Idris 语言具备堪与 Coq 媲美的交互式定理证明能力，自带 tactics，而其设计目标侧重于通用系统编程更甚于辅助证明。Idris 的其他设计目标还包括可观的代码性能，对副作用的控制，以及对于实现嵌入式领域特定语言（Embedded Domain Specific Language，EDSL）的支持。

Idris 语言使用 Haskell 编写实现，采用 BSD licenses 许可证。

[编辑] 功能

Theorem Proving（定理证明）
通过允许程序员描述对象语言的类型系统来帮助嵌入式 DSL 开发
Idris 2 is based on Quantitative Type Theory (QTT) 量化类型理论

[编辑] 指南

[编辑] 项目

Idris @ GitHub
相似项目:Coq, Agda

[编辑] 文档

Idris 2: Quantitative Type Theory in Action

[编辑] 图集

[编辑] 链接

Idris 官网

@@ 第11行： / 第11行： @@
 ==功能==
+*[https://idris2.readthedocs.io/en/latest/tutorial/theorems.html Theorem Proving（定理证明）]
+*通过允许程序员描述对象语言的类型系统来帮助嵌入式 DSL 开发
+*Idris 2 is based on [https://bentnib.org/quantitative-type-theory.html Quantitative Type Theory (QTT)] 量化类型理论
 ==指南==
 ==项目==
-*[[Coq]]
+*[https://github.com/idris-lang Idris @ GitHub]
-*[[Agda]]
+*相似项目:[[Coq]], [[Agda]]
+==文档==
+*[https://www.type-driven.org.uk/edwinb/papers/idris-qtt.pdf Idris 2: Quantitative Type Theory in Action]
 ==图集==
@@ 第22行： / 第28行： @@
 ==链接==
 *[http://idris-lang.org/ Idris 官网]
-*[https://github.com/idris-lang Idris @ GitHub]
 [[category:programming language]]