Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The current version of Agda was originally known as Agda 2. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version is a full rewrite, which should be considered a new language that shares a name and tradition. Agda is based on Zhaohui Luo's Unified Theory of Dependent Types (UTT) a type theory similar to Martin-Löf type theory.

Property Value
dbo:abstract
  • Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The current version of Agda was originally known as Agda 2. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version is a full rewrite, which should be considered a new language that shares a name and tradition. Agda, unlike Coq, has no support for tactics, and proofs are written in a functional programming style. The language has ordinary programming constructs such as data types, pattern matching, records, let expressions and modules, and a Haskell-like syntax. The system has an Emacs interface but can also be run in batch mode from the command line. Agda is based on Zhaohui Luo's Unified Theory of Dependent Types (UTT) a type theory similar to Martin-Löf type theory. (en)
  • Agda(アグダ)は定理証明器、すなわち数学的な証明を検証するコンピュータプログラムである。ペール・マルティン=レーフの型理論の一種における構成的証明構築のための対話的システムであり、一方で依存型をもつ関数型プログラミング言語であるともみなすことができる。1990年代よりチャルマース工科大学で主に開発されている。 他の定理証明支援系ではスクリプトによって「戦略」を指定して証明を操作するのに対して、Agda では証明を項として表し直接操作するというアイデアに基づいている。言語はデータ型や case式、シグネチャやレコードといった一般的なプログラミング構成概念をもつ。Emacsインターフェイスを使って対話的にコードを作成できるほか、直接コードをコンパイルする処理系の開発も進んでいる。 (ja)
  • Agda是一个依赖类型的函数式编程语言,同时亦可作为一个用于构建构造性证明的证明辅助工具。Agda最早由瑞典查尔摩斯工学院的 Ulf Norell 设计并开发,作为他的博士论文课题。目前的版本,Agda 2,则在第一版的基础上完全重写。 Agda体现了柯里-霍华德同构(Curry-Howard correspondence)。它的理论根基是 Zhaohui Luo 的UTT,该理论与 Per Martin-Löf 的直觉类型论相类似。 Agda与Coq的几点显著不同之处在于:它本身并不支持tactics;所有的证明均以函数式编程的方式书写;语言本身吸收了许多常规的程序语言元素,诸如:数据类型、模式匹配(pattern matching)、记录类型(records)、let表达式和模块(modules)等,而其语法则非常类似Haskell。 Agda系统一般通过其提供的Emacs界面进行交互,亦可藉由命令行方式单独执行。 (zh)
  • Agda — чистый функциональный язык программирования с зависимыми типами, то есть типами, которые могут быть индексированы значениями другого типа. Теоретической основой Agda служит интуиционистская теория типов Мартин-Лёфа (англ.), которая расширена набором конструкций, полезных для практического программирования. Agda также является системой автоматического доказательства. Логические высказывания записываются как типы, а доказательствами являются программы соответствующего типа. Agda поддерживает индуктивные типы данных, сопоставление с образцом (гибко использующее наличиезависимых типов), систему параметризованных модулей, проверку завершаемости программрусск., миксфиксный синтаксис для операторов. Поддержка неявных аргументов приводит к существенному упрощению программирования с зависимыми типами. Для программ на Agda характерно широкое использование Юникода. В стандартную реализацию Agda входит расширение редактора Emacs, позволяющее осуществлять пошаговое построение программ. Система проверки типов языка дает программисту полезную информацию о ещё не написанных частях программы. Конкретный синтаксис языка Agda весьма близок к синтаксису Haskell, на котором система Agda и реализована. (ru)
dbo:designer
dbo:developer
dbo:influenced
dbo:influencedBy
dbo:latestReleaseVersion
  • 2.5.1
dbo:license
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 4426773 (xsd:integer)
dbo:wikiPageRevisionID
  • 741332368 (xsd:integer)
dbp:fileExt
  • ,
dbp:operatingSystem
dbp:paradigm
dbp:writtenIn
  • Haskell
dct:subject
rdf:type
rdfs:comment
  • Agda(アグダ)は定理証明器、すなわち数学的な証明を検証するコンピュータプログラムである。ペール・マルティン=レーフの型理論の一種における構成的証明構築のための対話的システムであり、一方で依存型をもつ関数型プログラミング言語であるともみなすことができる。1990年代よりチャルマース工科大学で主に開発されている。 他の定理証明支援系ではスクリプトによって「戦略」を指定して証明を操作するのに対して、Agda では証明を項として表し直接操作するというアイデアに基づいている。言語はデータ型や case式、シグネチャやレコードといった一般的なプログラミング構成概念をもつ。Emacsインターフェイスを使って対話的にコードを作成できるほか、直接コードをコンパイルする処理系の開発も進んでいる。 (ja)
  • Agda是一个依赖类型的函数式编程语言,同时亦可作为一个用于构建构造性证明的证明辅助工具。Agda最早由瑞典查尔摩斯工学院的 Ulf Norell 设计并开发,作为他的博士论文课题。目前的版本,Agda 2,则在第一版的基础上完全重写。 Agda体现了柯里-霍华德同构(Curry-Howard correspondence)。它的理论根基是 Zhaohui Luo 的UTT,该理论与 Per Martin-Löf 的直觉类型论相类似。 Agda与Coq的几点显著不同之处在于:它本身并不支持tactics;所有的证明均以函数式编程的方式书写;语言本身吸收了许多常规的程序语言元素,诸如:数据类型、模式匹配(pattern matching)、记录类型(records)、let表达式和模块(modules)等,而其语法则非常类似Haskell。 Agda系统一般通过其提供的Emacs界面进行交互,亦可藉由命令行方式单独执行。 (zh)
  • Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The current version of Agda was originally known as Agda 2. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version is a full rewrite, which should be considered a new language that shares a name and tradition. Agda is based on Zhaohui Luo's Unified Theory of Dependent Types (UTT) a type theory similar to Martin-Löf type theory. (en)
  • Agda — чистый функциональный язык программирования с зависимыми типами, то есть типами, которые могут быть индексированы значениями другого типа. Теоретической основой Agda служит интуиционистская теория типов Мартин-Лёфа (англ.), которая расширена набором конструкций, полезных для практического программирования. Agda также является системой автоматического доказательства. Логические высказывания записываются как типы, а доказательствами являются программы соответствующего типа. Конкретный синтаксис языка Agda весьма близок к синтаксису Haskell, на котором система Agda и реализована. (ru)
rdfs:label
  • Agda (programming language) (en)
  • Agda (ja)
  • Agda (ru)
  • Agda (zh)
owl:sameAs
prov:wasDerivedFrom
foaf:homepage
foaf:isPrimaryTopicOf
foaf:name
  • Agda (en)
foaf:page
is dbo:influenced of
is dbo:influencedBy of
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is foaf:primaryTopic of