Agda

2021年12月20日 (一) 09:45的版本

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

Agda programming language

逻辑与计算之间最深刻的联系是一种双关。「命题即类型（Propositions as Types）」的学说断言，形式化的结构可以按两种方式看待：可以看做逻辑中的命题，也可以看做计算中的类型。（来自《编程语言基础：Agda 语言描述》）

文学编程（Literal Programming）是用带有代码的自然语言进行编程，文学编程自由地表达逻辑，此概念由高德纳（Donald Knuth）提出，希望能用来取代结构化编程范型。

可以用 Agda 证明助理编写的规范（Specification）同时描述了编程语言以及该语言编写的程序自身。

@@ 第19行： / 第19行： @@
 *[[Coq]]
 *[[Idris]]
+==图书==
+*[https://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?cPath=24&products_id=908 《Verified Functional Programming in Agda》]
 ==图集==