Agda

您可以在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） 同时描述了编程语言以及该语言编写的程序自身。

相似项目：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

指南

• 编程语言基础：Agda 语言描述
• Programming Language Foundations in Agda

项目

• Agda @ GitHub
• Univalent mathematics in Agda
• Libraries and other developments
• agda-prelude Programming library for Agda
• Cardano Formal ledger specifications

开发者

• 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

图书

• 《Verified Functional Programming in Agda》

STEM

• Courses using Agda
• Interactive Theorem Proving for Agda Users
• Computer Aided Formal Reasoning (G53CFR,G54CFR)

链接

• The Agda Wiki