Agda

Agda는 의존 타입 함수형 프로그래밍 언어이자 증명보조기이다.

Haskell의 영향을 받아 Haskell과 문법이 비슷하다. Agda의 컴파일러는 Haskell로 작성되어 있으며, 결과물로 Haskell 코드를 생성한다.

교재

Agda를 사용하는 프로그래밍 언어론 교재로 Programming Language Foundations in Agda가 있다.