Agda

您可以在Wikipedia上了解到此条目的英文信息 Agda Thanks, Wikipedia.

Agda programming language

简介

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

文学编程（Literal Programming）是用带有代码的自然语言进行编程，文学编程自由地表达逻辑，此概念由高德纳（Donald Knuth）提出，希望能用来取代结构化编程范型。

可以用 Agda 证明助理编写的规范（Specification） 同时描述了编程语言以及该语言编写的程序自身。

相似项目：Idris, Coq

功能

• Agda is a dependently typed functional programming language
• Agda is a proof assistant

指南

• 编程语言基础：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

图书

• 《Verified Functional Programming in Agda》

链接

• The Agda Wiki
• Agda @ GitHub