Agda

来自开放百科 - 灰狐
跳转到: 导航, 搜索
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

图集

链接

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

变换
操作
导航
工具箱