Agda
 | |
| 패러다임 | 함수형 |
|---|---|
| 설계자 | Ulf Norell; Catarina Coquand (1.0) |
| 개발자 | Ulf Norell; Catarina Coquand (1.0) |
| 발표일 | 2007년 (1.0 in 1999년) |
| 최근 버전 | 2.6.2 |
| 최근 버전 출시일 | 2021년 6월 19일 |
| 자료형 체계 | strong, static, dependent, nominal, manifest, inferred |
| 구현 언어 | Haskell |
| 운영 체제 | 크로스 플랫폼 |
| 라이선스 | BSD-like[1] |
| 파일 확장자 | .agda, .lagda, .lagda.md, .lagda.rst, .lagda.tex |
| 웹사이트 | wiki |
| 영향을 받은 언어 | |
| Coq, Epigram, Haskell | |
| 영향을 준 언어 | |
| Idris | |
Agda는 Chalmers University of Technology의 Ulf Norell의 박사 논문을 구현한 타입 종속적 함수형 프로그래밍 언어다.[2] 원래 Agda 시스템은 Catarina Coquand가 1999년 Chalmers에서 개발했다.[3] 원래 Agda 2로 알려진 현재 버전은 전체를 다시 작성했으며, 규칙과 이름을 공유하는 새로운 언어로 간주된다.
Agda는 커리-하워드 대응 패러다임에 기반한 증명 보조자(proof asistant)이며, Coq 와 달리 별도의 전술 언어가 아니고 증명은 함수형 프로그래밍 체계로 작성된다. 일반적인 프로그래밍 언어처럼 자료형, 패턴 매칭, 레코드, let 표현식 및 모듈, 하스켈 유사 구문이 있다. Emacs와 Atom에서 작동하는 인터페이스가 있고[4][5] 터미널에서 배치 모드로 실행할 수 있다.
Agda는 Zhaohui Luo의 unified theory of dependent types (UTT),[6] Martin-Löf 타입 이론 과 유사한 타입 이론을 기반으로 한다.
특징
[편집]유도 자료형
[편집]Agda에서는 주로 독립 자료형 프로그래밍 언어의 대수적 자료형과 유사한 유도 자료형(Inductive types)을 이용하여 자료형을 정의한다.
각주
[편집]- ↑ Agda license file
- ↑ Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007.
- ↑ “Agda: An Interactive Proof Editor”. 2011년 10월 8일에 원본 문서에서 보존된 문서. 2014년 10월 20일에 확인함.
- ↑ 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)에서 보존된 문서.
- ↑ “agda-mode on Atom”. 2017년 4월 7일에 확인함.
- ↑ Luo, Zhaohui. Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.
외부 링크
[편집]- Agda
- 공식 웹사이트
