Agda
- 프로그래밍 언어
- 함수형 프로그래밍 언어
- 증명 보조기
Agda는 의존 타입 함수형 프로그래밍 언어이자 증명보조기이다.
Haskell의 영향을 받아 Haskell과 문법이 비슷하다. Agda의 컴파일러는 Haskell로 작성되어 있으며, 결과물로 Haskell 코드를 생성한다.
교재
Programming Language Foundations in Agda
PLFA는 Agda를 이용한 프로그래밍 언어론 교재이다. 기초적인 Agda 증명법과 λ-계산의 실행 의미(operational semantics), 지시 의미(denotational semantics) 등을 다룬다.