欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜:Formal mathematics/Isabelle/ML, Formal verification/Coq/ACL2, C++/F#/Lisp
Agda
来自开放百科 - 灰狐
(版本间的差异)
(以“{{SeeWikipedia|Agda (programming language)}} right Agda programming language ==简介== ==功能== ==指南== ==项目== *相...”为内容创建页面) |
小 (→项目) |
||
(未显示1个用户的24个中间版本) | |||
第5行: | 第5行: | ||
==简介== | ==简介== | ||
+ | Agda is a dependently typed programming language / interactive theorem prover. | ||
+ | |||
+ | 逻辑与计算之间最深刻的联系是一种双关。「命题即类型(Propositions as Types)」 的学说断言,形式化的结构可以按两种方式看待:可以看做逻辑中的命题, 也可以看做计算中的类型。(来自《编程语言基础:Agda 语言描述》) | ||
+ | |||
+ | [https://zh.wikipedia.org/wiki/%E6%96%87%E5%AD%A6%E7%BC%96%E7%A8%8B 文学编程](Literal Programming)是用带有代码的自然语言进行编程,文学编程自由地表达逻辑,此概念由高德纳(Donald Knuth)提出,希望能用来取代结构化编程范型。 | ||
+ | |||
+ | 可以用 Agda 证明助理编写的规范(Specification) 同时描述了编程语言以及该语言编写的程序自身。 | ||
+ | |||
+ | 相似项目:[[Idris]], [[Coq]] | ||
+ | |||
+ | 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]] | ||
==指南== | ==指南== | ||
+ | *[https://agda-zh.github.io/PLFA-zh/ 编程语言基础:Agda 语言描述] | ||
+ | *[https://plfa.github.io/ Programming Language Foundations in Agda] | ||
==项目== | ==项目== | ||
− | * | + | *[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://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] [http://www.cse.chalmers.se/edu/course/DAT151/ Programming Language Technology] [https://github.com/InitialTypes/Club Initial Types Club] | ||
+ | |||
+ | ==文档== | ||
+ | *[https://hydra.iohk.io/build/12723913/download/1/paper.pdf System F in Agda] a formal model of System F in Agda | ||
+ | |||
+ | ==图书== | ||
+ | *[https://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?cPath=24&products_id=908 《Verified Functional Programming in Agda》] | ||
+ | |||
+ | ==STEM== | ||
+ | *[https://agda.readthedocs.io/en/v2.6.0.1/getting-started/tutorial-list.html Courses using Agda] | ||
+ | *[https://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/interactiveTheoremProvingForAgdaUsers.html Interactive Theorem Proving for Agda Users] | ||
+ | *[http://www.cs.nott.ac.uk/~psztxa/g53cfr/ Computer Aided Formal Reasoning (G53CFR,G54CFR)] | ||
==图集== | ==图集== | ||
==链接== | ==链接== | ||
+ | *[https://wiki.portal.chalmers.se/agda/pmwiki.php The Agda Wiki] | ||
+ | [[category:formal]] | ||
+ | [[category:proof assistant]] | ||
[[category:programming language]] | [[category:programming language]] | ||
+ | [[category:agda]] | ||
[[category:haskell]] | [[category:haskell]] | ||
+ | [[category:Huihoo Foundation]] |
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)
[编辑] 图集
[编辑] 链接
分享您的观点