Agda

이 문서는 토막글입니다.

토막글 규정을 유의하시기 바랍니다.

1. 개요2. 외부 링크

1. 개요

Martin-Löf의 의존타입이론(dependent type theory)에 기반한 함수형 언어이자 증명보조기. 프로그래밍 언어 Haskell의 영향을 받아 문법이 Haskell과 비슷하며, 구현 또한 Haskell로 되어있다.