欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜：Formal mathematics/Isabelle/ML, Formal verification/Coq/Agda, C++/Erlang/Lisp
Agda
来自开放百科 - 灰狐
（版本间的差异）
小 (→指南) |
小 (→项目) |
||
| 第31行： | 第31行： | ||
==项目== | ==项目== | ||
*[https://github.com/agda/agda Agda @ GitHub] | *[https://github.com/agda/agda Agda @ GitHub] | ||
| + | *[https://github.com/UniMath/agda-unimath Univalent mathematics in Agda] | ||
*[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 | ||
2022年10月12日 (三) 09:53的最后版本
|
您可以在Wikipedia上了解到此条目的英文信息 Agda Thanks, Wikipedia. |
Agda programming language
目录 |
[编辑] 简介
Agda is a dependently typed programming language / interactive theorem prover.
逻辑与计算之间最深刻的联系是一种双关。「命题即类型（Propositions as Types）」 的学说断言，形式化的结构可以按两种方式看待：可以看做逻辑中的命题， 也可以看做计算中的类型。（来自《编程语言基础：Agda 语言描述》）
文学编程（Literal Programming）是用带有代码的自然语言进行编程，文学编程自由地表达逻辑，此概念由高德纳（Donald Knuth）提出，希望能用来取代结构化编程范型。
可以用 Agda 证明助理编写的规范（Specification） 同时描述了编程语言以及该语言编写的程序自身。
Agda is
- a language for programs
- a language for their types
- a language for formulas
- a language for proofs
[编辑] 功能
- Agda is a dependently typed functional programming language
- Agda is a proof assistant
[编辑] 指南
[编辑] 项目
- Agda @ GitHub
- Univalent mathematics in Agda
- Libraries and other developments
- agda-prelude Programming library for Agda
[编辑] 开发者
- Ulf Norell
- Nils Anders Danielsson
- Jesper Cockx
- Andreas Abel Programming Language Technology Initial Types Club
[编辑] 文档
- System F in Agda a formal model of System F in Agda
[编辑] 图书
[编辑] STEM
- Courses using Agda
- Interactive Theorem Proving for Agda Users
- Computer Aided Formal Reasoning (G53CFR,G54CFR)
[编辑] 图集
[编辑] 链接
分享您的观点
