利用者:Foxtrot/Agda
| パラダイム | 関数型 |
|---|---|
| 最新リリース | 2.2.4/ 2009年7月7日 |
| 影響を受けた言語 | Coq, Epigram, Haskell |
| プラットフォーム | Cross-platform |
| ウェブサイト | Agda wiki |
| 拡張子 | .agda, .lagda |
Agdaは定理証明器、すなわち数学的な証明を検証するコンピュータプログラムである。特に、ペール・マルティン＝レーフの型理論の一種における構成的証明構築のための対話的システムである。これはチャルマース工科大学の博士研究員Ulf Norellによって開発され、依存型をもつ関数型プログラミング言語であるともみなすことができる。
Agdaは戦略的ではなく証明の項の直接的な操作というアイデアに基づいている。これによる証明は項であり、スクリプトではない。言語はデータ型やcase式、シグネチャやレコードといった一般的なプログラミング構成概念をもつ。システムはEmacsインターフェイスとグラフィカルインターフェイスAlfaをもつ。
Agda
[編集]Agdaの現在のバージョンであるAgda2は、Ulf Norellによってチャルマースで開発されている。インスタンス導出、文脈から推論できるときは省略できる暗黙の変数など、構文は Agda 1 から変更されている(ただし、変換ツールが開発されている)。Agda 2 はより可読性の高い証明を得るための方法として、Unicodeが広く使われている。
Agda 2 は Makoto Takeyama と Nils Anders Danielsson によって開発されたコマンドラインツールおよび強力なEmacsモードの両方を提供する。
10回目の Agda 実装者会議は2009年9月にヨーテボリで開催された。AIM11は3月に日本で開催が予定されている。
Agda 2 はEpigramに似ている。
参照
[編集]- C. Coquand et al. An Emacs interface for type directed support constructing proofs and programs. ENTCS 2006.
- A. Abel, et al. Verifying Haskell Programs Using Constructive Type Theory, ACM SIGPLAN Workshop Haskell'05, Tallinn, Estonia, 30 September 2005 http://www.tcs.informatik.uni-muenchen.de/~abel/haskell05.pdf
- M. Benke et al. Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing, 10(4):265-289, 2003. http://www.cs.chalmers.se/~marcin/Papers/universes.pdf
- T. Coquand et al. Connecting a Logical Framework to a First-Order Logic Prover. FroCos 2005, pp. 285-301.
外部リンク
[編集]- The Agda 2 homepage (wiki) ドキュメントとバグ報告ツールへのリンク
- Agda version 1 home page