이 문서는 토막글입니다. 토막글 규정을 유의하시기 바랍니다. 1. 개요2. 외부 링크1. 개요 Agda는 Martin-Löf의 의존타입이론(dependent type theory)에 기반한 함수형 언어이자 증명보조기이다. 프로그래밍 언어 Haskell의 영향을 받아 문법이 Haskell과 비슷하며 구현 또한 Haskell로 되어있다. 2. 외부 링크 The Agda Wiki 분류 증명보조기 함수형 언어