Agda (programming language) (original) (raw)
Agda는 Chalmers University of Technology의 Ulf Norell의 박사 논문을 구현한 타입 종속적 함수형 프로그래밍 언어다. 원래 Agda 시스템은 Catarina Coquand가 1999년 Chalmers에서 개발했다. 원래 Agda 2로 알려진 현재 버전은 전체를 다시 작성했으며, 규칙과 이름을 공유하는 새로운 언어로 간주된다. Agda는 커리-하워드 대응 패러다임에 기반한 증명 보조자(proof asistant)이며, Coq 와 달리 별도의 전술 언어가 아니고 증명은 함수형 프로그래밍 체계로 작성된다. 일반적인 프로그래밍 언어처럼 자료형, 패턴 매칭, 레코드, let 표현식 및 모듈, 하스켈 유사 구문이 있다. Emacs와 Atom에서 작동하는 인터페이스가 있고 터미널에서 배치 모드로 실행할 수 있다. Agda는 Zhaohui Luo의 unified theory of dependent types (UTT), Martin-Löf 타입 이론 과 유사한 타입 이론을 기반으로 한다.
| 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 original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version, originally known as Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition. Agda is also a proof assistant based on the propositions-as-types paradigm, but unlike Coq, has no separate language, 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 Emacs and Atom interfaces but can also be run in batch mode from the command line. Agda is based on Zhaohui Luo's (UTT), a type theory similar to Martin-Löf type theory. Agda is named after the Swedish song "Hönan Agda", written by Cornelis Vreeswijk, which is about a hen named Agda. This alludes to the naming of Coq. (en) Το Agda είναι (proof assistant), δηλ. ένα πρόγραμμα υπολογιστή που μπορεί να ελέγχει μαθηματικές αποδείξεις. Αποτελεί ένα για την ανάπτυξη σε μια παραλλαγή της Ιντουισιονιστικής Θεωρίας Τύπων του Περ Μάρτιν-Λεφ (Per Martin-Löf). Μπορεί να θεωρηθεί γλώσσα συναρτησιακού προγραμματισμού με εξαρτώμενους τύπους. Το Agda αναπτύχθηκε από τον Ουλφ Νόρελ, μεταδιδακτορικό ερευνητή του Πανεπιστημίου Τεχνολογίας του Τσάλμερς (Chalmers University of Technology). Το Agda βασίζεται στην ιδέα του απευθείας χειρισμού των όρων μιας απόδειξης, και όχι στις τακτικές (tactics): μια απόδειξη είναι όρος, όχι σενάριο με τακτικές. Η γλώσσα έχει κλασικές προγραμματιστικές δομές, όπως οι τύποι δεδομένων και οι εκφράσεις ανάλυσής τους (case-expressions), οι υπογραφές (signatures) και οι εγγραφές (records), οι εκφράσεις let και οι μονάδες κώδικα (modules). Το σύστημα παρέχει μια διεπαφή για τον διορθωτή Emacs και μια γραφική διεπαφή, την Alfa. (el) Agda는 Chalmers University of Technology의 Ulf Norell의 박사 논문을 구현한 타입 종속적 함수형 프로그래밍 언어다. 원래 Agda 시스템은 Catarina Coquand가 1999년 Chalmers에서 개발했다. 원래 Agda 2로 알려진 현재 버전은 전체를 다시 작성했으며, 규칙과 이름을 공유하는 새로운 언어로 간주된다. Agda는 커리-하워드 대응 패러다임에 기반한 증명 보조자(proof asistant)이며, Coq 와 달리 별도의 전술 언어가 아니고 증명은 함수형 프로그래밍 체계로 작성된다. 일반적인 프로그래밍 언어처럼 자료형, 패턴 매칭, 레코드, let 표현식 및 모듈, 하스켈 유사 구문이 있다. Emacs와 Atom에서 작동하는 인터페이스가 있고 터미널에서 배치 모드로 실행할 수 있다. Agda는 Zhaohui Luo의 unified theory of dependent types (UTT), Martin-Löf 타입 이론 과 유사한 타입 이론을 기반으로 한다. (ko) Agda（アグダ）は、定理証明器、すなわち数学的な証明を検証するコンピュータプログラムであり、ペール・マルティン＝レーフの型理論の一種における構成的証明構築のための対話的システムである。機能的には、依存型をもつ関数型プログラミング言語であるともみなすこともできる。1990年代よりチャルマース工科大学で主に開発されている。 他の定理証明支援系ではスクリプトによって「タクティク」(tactic)を指定して証明を操作するのに対して、Agda では証明を項として表し直接操作するというアイデアに基づいている。言語はデータ型や case式、シグネチャやレコードといった一般的なプログラミング構成概念をもつ。Emacsインターフェイスを使って対話的にコードを作成できるほか、直接コードをコンパイルする処理系の開発も進んでいる。 (ja) Agda is een afhankelijk getypeerde functionele programmeertaal, oorspronkelijk ontwikkeld door Ulf Norell aan de Technische Universiteit Chalmers. Agda is niet Turingvolledig. (nl) Agda 是一个依赖类型的纯函数式编程语言。目前的版本，Agda 2，最初由瑞典查尔摩斯工学院的 Ulf Norell 作为博士论文课题设计并实现。先前的版本 Agda 1 由 Catarina Coquand 在 1999 年开发，而现今的版本则是对其的彻底重写，因此可视作一个全新的语言，但保留了 Agda 的命名和传统。 Agda 的类型系统体现了柯里-霍华德同构（Curry-Howard correspondence），因此亦可作为一个构建构造性证明的。它的类型理论基于 Zhaohui Luo 提出的 UTT（unified theory of dependent types），与 Per Martin-Löf 的直觉类型论相似。 Agda 与另一个基于依赖类型的证明辅助工具 Coq 设计上存在着显著的不同之处：它本身并不提供单独的证明策略语言（tactics），所有的证明均以函数式编程的方式书写；Agda 拥有许多常规的函数式程序语言要素，诸如：数据类型（data types）、模式匹配（pattern matching）、记录类型（records）、let表达式和模块（modules）等，而其语法设计则高度仿照 Haskell 语言。 用户可通过 Emacs 或 Atom 编辑器的界面与 Agda 系统进行交互。Agda 系统亦可藉由命令行单独调用。 通过类型检查的 Agda 程序可以被编译到 Haskell，并由 GHC 编译器最终编译为可执行的本地机器码；亦有编译到 JavaScript 的后端实现。 Agda 的名字来自于一首由音乐家 Cornelis Vreeswijk 创作的瑞典语歌曲“Hönan Agda”，歌词讲述了一只名叫 Agda 的母鸡的故事。这实际上影射了 Coq（Coq 在法语中意为公鸡）。 (zh) Agda — чистый функциональный язык программирования с зависимыми типами, то есть типами, которые могут быть индексированы значениями другого типа. Теоретической основой Agda служит интуиционистская теория типов Мартин-Лёфа, которая расширена набором конструкций, полезных для практического программирования. Agda также является системой автоматического доказательства. Логические высказывания записываются как типы, а доказательствами являются программы соответствующего типа. Agda поддерживает индуктивные типы данных, сопоставление с образцом (гибко использующее наличиезависимых типов), систему параметризованных модулей, проверку завершаемости программ, миксфиксный синтаксис для операторов. Поддержка неявных аргументов приводит к существенному упрощению программирования с зависимыми типами. Для программ на Agda характерно широкое использование Юникода. В стандартную реализацию Agda входит расширение редактора Emacs, позволяющее осуществлять пошаговое построение программ. Система проверки типов языка дает программисту полезную информацию о ещё не написанных частях программы. Конкретный синтаксис языка Agda весьма близок к синтаксису Haskell, на котором система Agda и реализована. (ru) Agda - вільна функціональна мова програмування створена 2007 року, під впливом Coq, та Haskell. (uk) |
| dbo:thumbnail | wiki-commons:Special:FilePath/Agda's_official_logo.svg?width=300 |
| dbo:wikiPageExternalLink | http://oxij.org/note/BrutalDepTypes/ http://people.inf.elte.hu/divip/AgdaTutorial/Index.html https://www.youtube.com/playlist%3Fp=B7F836675DCE009C http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf http://www.cse.chalmers.se/~ulfn/papers/tphols09/tutorial.pdf |
| dbo:wikiPageID | 4426773 (xsd:integer) |
| dbo:wikiPageLength | 12677 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1106676407 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Dependent_type dbr:Peano_axioms dbr:Unicode dbr:Intuitionistic_type_theory dbr:Let_expression dbc:2007_software dbc:Functional_languages dbr:Coq dbr:Cornelis_Vreeswijk dbr:Cross-platform dbr:Chicken dbr:Emacs dbr:Epigram_(programming_language) dbr:Static_typing dbr:Functional_programming dbr:Successor_function dbr:Total_functional_programming dbr:BSD_licenses dbc:Cross-platform_free_software dbc:Chalmers_University_of_Technology dbc:Free_software_programmed_in_Haskell dbc:Haskell_programming_language_family dbc:Programming_languages_created_in_2007 dbr:Ada_(programming_language) dbr:Algebraic_data_type dbr:Data_type dbr:Record_(computer_science) dbr:HOL_(proof_assistant) dbr:Haskell_(programming_language) dbr:Isabelle_(proof_assistant) dbr:JavaScript dbr:Termination_checking dbr:Atom_(text_editor) dbc:Academic_programming_languages dbc:Dependently_typed_languages dbc:Free_compilers_and_interpreters dbc:Pattern_matching_programming_languages dbc:Programming_languages dbc:Proof_assistants dbc:Statically_typed_programming_languages dbr:Chalmers_University_of_Technology dbr:Swedish_language dbr:Dependent_typing dbr:Inferred_typing dbr:Nominal_typing dbr:Idris_(programming_language) dbr:Inductive_type dbr:Reflection_(computer_programming) dbr:Pattern_matching dbr:Manifest_typing dbr:Strong_typing dbr:Propositions-as-types dbr:Tactic_(computer_science) dbr:Unified_theory_of_dependent_types |
| dbp:designer | Ulf Norell; Catarina Coquand (en) |
| dbp:developer | Ulf Norell; Catarina Coquand (en) |
| dbp:fileExt | , , , , (en) |
| dbp:influenced | dbr:Idris_(programming_language) |
| dbp:influencedBy | dbr:Coq dbr:Epigram_(programming_language) dbr:Haskell_(programming_language) |
| dbp:latestReleaseDate | 2021-06-19 (xsd:date) |
| dbp:latestReleaseVersion | 2.600000 (xsd:double) |
| dbp:license | dbr:BSD_licenses |
| dbp:logo | Agda's official logo.svg (en) |
| dbp:logoAlt | A stylized chicken in black lines and dots, to the left of the name "Agda" in sans-serif test with the first letter slanted to the right. (en) |
| dbp:name | Agda (en) |
| dbp:operatingSystem | dbr:Cross-platform |
| dbp:paradigm | dbr:Functional_programming |
| dbp:programmingLanguage | dbr:Haskell_(programming_language) |
| dbp:typing | dbr:Static_typing dbr:Dependent_typing dbr:Inferred_typing dbr:Nominal_typing dbr:Manifest_typing dbr:Strong_typing |
| dbp:wikiPageUsesTemplate | dbt:Cite_web dbt:Distinguish dbt:Infobox_programming_language dbt:Official_website dbt:Reflist dbt:Short_description dbt:Start_date_and_age dbt:URL dbt:Bracket dbt:Projects_at_Chalmers_University_of_Technology |
| dct:subject | dbc:2007_software dbc:Functional_languages dbc:Cross-platform_free_software dbc:Chalmers_University_of_Technology dbc:Free_software_programmed_in_Haskell dbc:Haskell_programming_language_family dbc:Programming_languages_created_in_2007 dbc:Academic_programming_languages dbc:Dependently_typed_languages dbc:Free_compilers_and_interpreters dbc:Pattern_matching_programming_languages dbc:Programming_languages dbc:Proof_assistants dbc:Statically_typed_programming_languages |
| rdf:type | owl:Thing dbo:Software yago:Abstraction100002137 yago:ArtificialLanguage106894544 yago:Communication100033020 yago:Language106282651 yago:ProgrammingLanguage106898352 yago:WikicatFunctionalLanguages yago:WikicatDependentlyTypedLanguages |
| rdfs:comment | Agda는 Chalmers University of Technology의 Ulf Norell의 박사 논문을 구현한 타입 종속적 함수형 프로그래밍 언어다. 원래 Agda 시스템은 Catarina Coquand가 1999년 Chalmers에서 개발했다. 원래 Agda 2로 알려진 현재 버전은 전체를 다시 작성했으며, 규칙과 이름을 공유하는 새로운 언어로 간주된다. Agda는 커리-하워드 대응 패러다임에 기반한 증명 보조자(proof asistant)이며, Coq 와 달리 별도의 전술 언어가 아니고 증명은 함수형 프로그래밍 체계로 작성된다. 일반적인 프로그래밍 언어처럼 자료형, 패턴 매칭, 레코드, let 표현식 및 모듈, 하스켈 유사 구문이 있다. Emacs와 Atom에서 작동하는 인터페이스가 있고 터미널에서 배치 모드로 실행할 수 있다. Agda는 Zhaohui Luo의 unified theory of dependent types (UTT), Martin-Löf 타입 이론 과 유사한 타입 이론을 기반으로 한다. (ko) Agda（アグダ）は、定理証明器、すなわち数学的な証明を検証するコンピュータプログラムであり、ペール・マルティン＝レーフの型理論の一種における構成的証明構築のための対話的システムである。機能的には、依存型をもつ関数型プログラミング言語であるともみなすこともできる。1990年代よりチャルマース工科大学で主に開発されている。 他の定理証明支援系ではスクリプトによって「タクティク」(tactic)を指定して証明を操作するのに対して、Agda では証明を項として表し直接操作するというアイデアに基づいている。言語はデータ型や case式、シグネチャやレコードといった一般的なプログラミング構成概念をもつ。Emacsインターフェイスを使って対話的にコードを作成できるほか、直接コードをコンパイルする処理系の開発も進んでいる。 (ja) Agda is een afhankelijk getypeerde functionele programmeertaal, oorspronkelijk ontwikkeld door Ulf Norell aan de Technische Universiteit Chalmers. Agda is niet Turingvolledig. (nl) Agda - вільна функціональна мова програмування створена 2007 року, під впливом Coq, та Haskell. (uk) 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 original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version, originally known as Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition. Agda is based on Zhaohui Luo's (UTT), a type theory similar to Martin-Löf type theory. (en) Το Agda είναι (proof assistant), δηλ. ένα πρόγραμμα υπολογιστή που μπορεί να ελέγχει μαθηματικές αποδείξεις. Αποτελεί ένα για την ανάπτυξη σε μια παραλλαγή της Ιντουισιονιστικής Θεωρίας Τύπων του Περ Μάρτιν-Λεφ (Per Martin-Löf). Μπορεί να θεωρηθεί γλώσσα συναρτησιακού προγραμματισμού με εξαρτώμενους τύπους. Το Agda αναπτύχθηκε από τον Ουλφ Νόρελ, μεταδιδακτορικό ερευνητή του Πανεπιστημίου Τεχνολογίας του Τσάλμερς (Chalmers University of Technology). (el) Agda — чистый функциональный язык программирования с зависимыми типами, то есть типами, которые могут быть индексированы значениями другого типа. Теоретической основой Agda служит интуиционистская теория типов Мартин-Лёфа, которая расширена набором конструкций, полезных для практического программирования. Agda также является системой автоматического доказательства. Логические высказывания записываются как типы, а доказательствами являются программы соответствующего типа. Конкретный синтаксис языка Agda весьма близок к синтаксису Haskell, на котором система Agda и реализована. (ru) Agda 是一个依赖类型的纯函数式编程语言。目前的版本，Agda 2，最初由瑞典查尔摩斯工学院的 Ulf Norell 作为博士论文课题设计并实现。先前的版本 Agda 1 由 Catarina Coquand 在 1999 年开发，而现今的版本则是对其的彻底重写，因此可视作一个全新的语言，但保留了 Agda 的命名和传统。 Agda 的类型系统体现了柯里-霍华德同构（Curry-Howard correspondence），因此亦可作为一个构建构造性证明的。它的类型理论基于 Zhaohui Luo 提出的 UTT（unified theory of dependent types），与 Per Martin-Löf 的直觉类型论相似。 Agda 与另一个基于依赖类型的证明辅助工具 Coq 设计上存在着显著的不同之处：它本身并不提供单独的证明策略语言（tactics），所有的证明均以函数式编程的方式书写；Agda 拥有许多常规的函数式程序语言要素，诸如：数据类型（data types）、模式匹配（pattern matching）、记录类型（records）、let表达式和模块（modules）等，而其语法设计则高度仿照 Haskell 语言。 用户可通过 Emacs 或 Atom 编辑器的界面与 Agda 系统进行交互。Agda 系统亦可藉由命令行单独调用。 (zh) |
| rdfs:label | Agda (el) Agda (programming language) (en) Agda (ja) Agda (ko) Agda (nl) Agda (ru) Agda (uk) Agda (zh) |
| owl:sameAs | freebase:Agda (programming language) yago-res:Agda (programming language) wikidata:Agda (programming language) dbpedia-el:Agda (programming language) dbpedia-fa:Agda (programming language) dbpedia-ja:Agda (programming language) dbpedia-ko:Agda (programming language) dbpedia-nl:Agda (programming language) dbpedia-ru:Agda (programming language) dbpedia-uk:Agda (programming language) dbpedia-zh:Agda (programming language) https://global.dbpedia.org/id/wjGc |
| prov:wasDerivedFrom | wikipedia-en:Agda_(programming_language)?oldid=1106676407&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/Agda's_official_logo.svg |
| foaf:homepage | http://wiki.portal.chalmers.se/agda |
| foaf:isPrimaryTopicOf | wikipedia-en:Agda_(programming_language) |
| is dbo:influenced of | dbr:Epigram_(programming_language) dbr:Haskell |
| is dbo:influencedBy of | dbr:Idris_(programming_language) |
| is dbo:wikiPageDisambiguates of | dbr:Agda |
| is dbo:wikiPageRedirects of | dbr:Agda_theorem_prover dbr:Agda2 dbr:Agda_(proof_assistant) dbr:Agda_(theorem_prover) |
| is dbo:wikiPageWikiLink of | dbr:Proof_assistant dbr:List_of_arbitrary-precision_arithmetic_software dbr:List_of_filename_extensions_(A–E) dbr:Applicative_functor dbr:Characters_per_line dbr:Univalent_foundations dbr:Induction-recursion dbr:Intuitionistic_logic dbr:List_of_programming_languages_by_type dbr:Coq dbr:Generational_list_of_programming_languages dbr:Epigram_(programming_language) dbr:Comparison_of_programming_languages_by_type_system dbr:Timeline_of_programming_languages dbr:Type_theory dbr:Haskell dbr:Isabelle_(proof_assistant) dbr:ALF_(proof_assistant) dbr:Agda dbr:Agda_theorem_prover dbr:Lean_(proof_assistant) dbr:Blakers–Massey_theorem dbr:Referential_transparency dbr:Termination_analysis dbr:Idris_(programming_language) dbr:Literate_programming dbr:First-class_citizen dbr:Agda2 dbr:Agda_(proof_assistant) dbr:Agda_(theorem_prover) |
| is dbp:influenced of | dbr:Epigram_(programming_language) |
| is dbp:influencedBy of | dbr:Idris_(programming_language) |
| is foaf:primaryTopic of | wikipedia-en:Agda_(programming_language) |
