Agda: 두 판 사이의 차이

{{프로그래밍 언어 정보|name=Agda|typing=[[Strong typing|strong]], [[Static typing|static]], [[Dependent typing|dependent]], [[Nominal typing|nominal]], [[Manifest typing|manifest]], [[Inferred typing|inferred]]|operating system=[[크로스 플랫폼]]|file ext=<code>.agda</code>, <code>.lagda</code>, <code>.lagda.md</code>, <code>.lagda.rst</code>, <code>.lagda.tex</code>|license=[[BSD licenses|BSD-like]]<ref>[http://code.haskell.org/Agda/LICENSE Agda license file]</ref>|influenced by=[[Coq]], [[Epigram (programming language)|Epigram]], [[Haskell (programming language)|Haskell]]|programming language=[[Haskell (programming language)|Haskell]]|influenced=[[Idris (programming language)|Idris]]|dialects=|implementations=|latest test date=|logo=Agda's official logo.svg|latest test version=|latest release date={{시작 날짜와 나이|2019|05|17}}|latest release version=2.6.0.1|developer=Ulf Norell; Catarina Coquand (1.0)|designer=Ulf Norell; Catarina Coquand (1.0)|year={{시작 날짜와 나이|2007}} (1.0 in {{시작 날짜와 나이|1999}})|paradigm=[[함수형 프로그래밍|함수형]]|logo alt=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.|website={{URL|wiki.portal.chalmers.se/agda}}}}

 

 

Agda는 [[커리-하워드 대응]] 패러다임에 기반한 증명 보조자(proof asistant)이며, Coq 와 달리 별도의 전술 언어가 아니고 증명은 함수형 프로그래밍 체계로 작성된다. 일반적인 프로그래밍 언어처럼 [[자료형]], [[패턴 매칭]], [[레코드 (컴퓨터 과학)|레코드]], let 표현식 및 모듈, [[하스켈]] 유사 구문이 있다. [[이맥스|Emacs]]와 [[아톰 (문서 편집기)|Atom]]에서 작동하는 인터페이스가 있고<ref name="emacs-mode">{{콘퍼런스 인용|first1=Catarina|last1=Coquand|first2=Dan|last2=Synek|first3=Makoto|last3=Takeyama|title=An Emacs interface for type directed support constructing proofs and programs|conference=European Joint Conferences on Theory and Practice of Software 2005|url=https://mailserver.di.unipi.it/ricerca/proceedings/ETAPS05/uitp/uitp_p05.pdf|archive-url=https://web.archive.org/web/20110722063632/https://mailserver.di.unipi.it/ricerca/proceedings/ETAPS05/uitp/uitp_p05.pdf|url-status=dead|archive-date=2011-07-22}}</ref><ref>{{웹 인용|url=https://atom.io/packages/agda-mode|제목=agda-mode on Atom|확인날짜=7 April 2017}}</ref> 터미널에서 배치 모드로 실행할 수 있다.