Agda는 Chalmers University of Technology의 Ulf Norell의 박사 논문을 구현한 타입 종속적 함수형 프로그래밍 언어다.[2] 원래 Agda 시스템은 Catarina Coquand가 1999년 Chalmers에서 개발했다.[3] 원래 Agda 2로 알려진 현재 버전은 전체를 다시 작성했으며, 규칙과 이름을 공유하는 새로운 언어로 간주된다.

Agda
A stylized chicken in black lines and dots, to the left of the name “Agda” in sans-serif test with the first letter slanted to the right.
패러다임함수형
설계자Ulf Norell; Catarina Coquand (1.0)
개발자Ulf Norell; Catarina Coquand (1.0)
발표일2007년(15년 전)(2007) (1.0 in 1999년(23년 전)(1999))
최근 버전2.6.0.1
최근 버전 출시일2019년 5월 17일(3년 전)(2019-05-17)
자료형 체계strong, static, dependent, nominal, manifest, inferred
구현 언어Haskell
운영 체제크로스 플랫폼
라이선스BSD-like[1]
파일 확장자.agda, .lagda, .lagda.md, .lagda.rst, .lagda.tex
웹사이트wiki.portal.chalmers.se/agda
영향을 받은 언어
Coq, Epigram, Haskell
영향을 준 언어
Idris

Agda는 커리-하워드 대응 패러다임에 기반한 증명 보조자(proof asistant)이며, Coq 와 달리 별도의 전술 언어가 아니고 증명은 함수형 프로그래밍 체계로 작성된다. 일반적인 프로그래밍 언어처럼 자료형, 패턴 매칭, 레코드, let 표현식 및 모듈, 하스켈 유사 구문이 있다. EmacsAtom에서 작동하는 인터페이스가 있고[4][5] 터미널에서 배치 모드로 실행할 수 있다.

Agda는 Zhaohui Luo의 unified theory of dependent types (UTT),[6] Martin-Löf 타입 이론 과 유사한 타입 이론을 기반으로 한다.

특징편집

유도 자료형편집

Agda에서는 주로 독립 자료형 프로그래밍 언어의 대수적 자료형과 유사한 유도 자료형(Inductive types)을 이용하여 자료형을 정의한다.

각주편집

  1. Agda license file
  2. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007.
  3. “Agda: An Interactive Proof Editor”. 2011년 10월 8일에 원본 문서에서 보존된 문서. 2014년 10월 20일에 확인함. 
  4. Coquand, Catarina; Synek, Dan; Takeyama, Makoto. 《An Emacs interface for type directed support constructing proofs and programs》 (PDF). European Joint Conferences on Theory and Practice of Software 2005. 2011년 7월 22일에 원본 문서 (PDF)에서 보존된 문서. 
  5. “agda-mode on Atom”. 2017년 4월 7일에 확인함. 
  6. Luo, Zhaohui. Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.

외부 링크편집

  • Agda - 공식 웹사이트