Agda: 두 판 사이의 차이
내용 삭제됨 내용 추가됨
편집 요약 없음 |
|||
1번째 줄:
{{위키데이터 속성 추적}}
{{프로그래밍 언어 정보|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 | latest release date = {{ |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'''는 Chalmers University of Technology의 Ulf Norell의 박사 논문을 구현한 타입 종속적 [[함수형 프로그래밍]] 언어다.<ref>Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007.</ref> 원래 Agda 시스템은 Catarina Coquand가 1999년 Chalmers에서 개발했다.<ref>{{웹 인용|url=http://ocvs.cfv.jp/Agda/index.html|제목=Agda: An Interactive Proof Editor|보존url=https://web.archive.org/web/20111008115843/http://ocvs.cfv.jp/Agda/index.html|보존날짜=2011-10-08|url-status=dead|확인날짜=2014-10-20}}</ref> 원래 Agda 2로 알려진 현재 버전은 전체를 다시 작성했으며, 규칙과 이름을 공유하는 새로운 언어로 간주된다.
| |||