Agda

来自开放百科 - 灰狐
(版本间的差异)
跳转到: 导航, 搜索
(简介)
(项目)
 
(未显示1个用户的4个中间版本)
第5行: 第5行:
  
 
==简介==
 
==简介==
逻辑与计算之间最深刻的联系是一种双关。「命题即类型(Propositions as Types)」 的学说断言,形式化的结构可以按两种方式看待:可以看做逻辑中的命题, 也可以看做计算中的类型。(来自《编程语言基础:Agda 语言描述》)
+
Agda is a dependently typed programming language / interactive theorem prover.
  
Agda is a proof assistant.
+
逻辑与计算之间最深刻的联系是一种双关。「命题即类型(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)提出,希望能用来取代结构化编程范型。
 
[https://zh.wikipedia.org/wiki/%E6%96%87%E5%AD%A6%E7%BC%96%E7%A8%8B 文学编程](Literal Programming)是用带有代码的自然语言进行编程,文学编程自由地表达逻辑,此概念由高德纳(Donald Knuth)提出,希望能用来取代结构化编程范型。
第27行: 第27行:
 
==指南==
 
==指南==
 
*[https://agda-zh.github.io/PLFA-zh/ 编程语言基础:Agda 语言描述]
 
*[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/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
第46行: 第48行:
  
 
==STEM==
 
==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]
 
*[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)]
  
 
==图集==
 
==图集==

2022年10月12日 (三) 09:53的最后版本

Wikipedia-35x35.png 您可以在Wikipedia上了解到此条目的英文信息 Agda Thanks, Wikipedia.
Agda-language-logo.png

Agda programming language

目录

[编辑] 简介

Agda is a dependently typed programming language / interactive theorem prover.

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

文学编程(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

[编辑] 功能

[编辑] 指南

[编辑] 项目

[编辑] 开发者

[编辑] 文档

[编辑] 图书

[编辑] STEM

[编辑] 图集

[编辑] 链接

分享您的观点
个人工具
名字空间

变换
操作
导航
工具箱