Agda

Agda（アグダ）は、定理証明器、すなわち数学的な証明を検証するコンピュータプログラムであり、ペール・マルティン＝レーフの型理論の一種における構成的証明構築のための対話的システムである。機能的には、依存型をもつ関数型プログラミング言語であるともみなすこともできる。1990年代よりチャルマース工科大学で主に開発されている。 他の定理証明支援系ではスクリプトによって「タクティク」(tactic)を指定して証明を操作するのに対して、Agda では証明を項として表し直接操作するというアイデアに基づいている。言語はデータ型や case式、シグネチャやレコードといった一般的なプログラミング構成概念をもつ。Emacsインターフェイスを使って対話的にコードを作成できるほか、直接コードをコンパイルする処理系の開発も進んでいる。