Agda言語

Agda言語は、いわゆる函数型プログラミング言語です。
Agda言語で、論理式やその証明を記すこともできます。
- - Agda言語は「強い型付」を持つ言語です。しかも、その型システムは「依存型」と言われるものを含むため、型を述語、その型の要素を述語の証明と見なすことができます（いわゆる型としての論理式、formulae as types）