欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜:Formal mathematics/Isabelle/ML, Formal verification/Coq/Agda, C++/Erlang/Lisp
Agda
来自开放百科 - 灰狐
(版本间的差异)
小 (→功能) |
小 (→图书) |
||
第23行: | 第23行: | ||
*[https://wiki.portal.chalmers.se/agda/Main/Libraries Libraries and other developments] | *[https://wiki.portal.chalmers.se/agda/Main/Libraries Libraries and other developments] | ||
*[https://github.com/UlfNorell/agda-prelude agda-prelude] Programming library for Agda | *[https://github.com/UlfNorell/agda-prelude agda-prelude] Programming library for Agda | ||
+ | |||
+ | ==开发者== | ||
+ | *[http://www.cse.chalmers.se/~ulfn/ Ulf Norell] | ||
+ | *[http://www.cse.chalmers.se/~nad/ Nils Anders Danielsson] | ||
+ | *[https://jesper.sikanda.be/ Jesper Cockx] | ||
+ | *[http://www.cse.chalmers.se/~abela/ Andreas Abel] | ||
==图书== | ==图书== |
2022年2月8日 (二) 05:07的版本
您可以在Wikipedia上了解到此条目的英文信息 Agda Thanks, Wikipedia. |
Agda programming language
目录 |
简介
逻辑与计算之间最深刻的联系是一种双关。「命题即类型(Propositions as Types)」 的学说断言,形式化的结构可以按两种方式看待:可以看做逻辑中的命题, 也可以看做计算中的类型。(来自《编程语言基础:Agda 语言描述》)
文学编程(Literal Programming)是用带有代码的自然语言进行编程,文学编程自由地表达逻辑,此概念由高德纳(Donald Knuth)提出,希望能用来取代结构化编程范型。
可以用 Agda 证明助理编写的规范(Specification) 同时描述了编程语言以及该语言编写的程序自身。
功能
- Agda is a dependently typed functional programming language
- Agda is a proof assistant
指南
项目
- Libraries and other developments
- agda-prelude Programming library for Agda
开发者
图书
图集
链接
分享您的观点