Agda

Agda는 타입이 프로그램 값에 의존할 수 있는 의존 타입을 중심으로 설계된 함수형 프로그래밍 언어이자 대화형 정리 증명 도구다. Martin-Löf 타입 이론의 영향을 바탕으로 프로그램의 성질을 타입으로 표현하고 증명 항을 작성할 수 있으며, 함수 정의·패턴 일치·귀납적 자료형과 대화...

분류	의존 타입 기반 함수형 프로그래밍 언어, 증명 보조기
설계	Ulf Norell을 중심으로 발전
이론적 기반	Martin-Löf 타입 이론
주요 기능	의존 타입, 패턴 일치, 귀납적 자료형, 대화형 증명
관련 언어	Idris, Lean, Coq

Agda는 타입이 프로그램 값에 의존할 수 있는 의존 타입을 중심으로 설계된 함수형 프로그래밍 언어이자 대화형 정리 증명 도구다. Martin-Löf 타입 이론의 영향을 바탕으로 프로그램의 성질을 타입으로 표현하고 증명 항을 작성할 수 있으며, 함수 정의·패턴 일치·귀납적 자료형과 대화형 구멍 채우기(Hole-driven Development)를 결합한다. Ulf Norell 등이 발전시킨 Agda는 정적 타입 시스템 연구와 형식 검증, 구성적 수학의 정형화에 사용된다.^[1]

역사

Chalmers의 타입 이론 연구

Ulf Norell과 현대 Agda

버전과 개발 생태계

언어 설계

의존 타입과 타입 계층

함수와 패턴 일치

귀납적 자료형과 레코드

모듈과 이름 공간

증명과 검증

명제와 타입의 대응

정의의 완전성과 종료 검사

대화형 증명 개발

컴파일과 실행 환경

타입 검사기와 편집기 연동

백엔드와 실행 코드

표준 라이브러리

활용과 영향

형식화된 수학

검증 가능한 프로그램