Agda言語


Agda言語とは?

  • Agda言語は、いわゆる函数型プログラミング言語です。
  • Agda言語で、論理式やその証明を記すこともできます。
    • Agda言語は「強い型付」を持つ言語です。しかも、その型システムは「依存型」と言われるものを含むため、型を述語、その型の要素を述語の証明と見なすことができます(いわゆる型としての論理式、formulae as types)
  • 詳しい情報が Agda wiki にあります。’Agda wiki' を検索してみてください。