ALF(프루프 어시스턴트)
ALF (proof assistant)ALF(다른 논리적 프레임워크)는 Chalmers University에서 개발된 단일 동형 Martin-Löf 유형 이론의 구조 편집자입니다.알파, 아그다, 카이엔 및 Coq 인증 보조 프로그램 및 의존적으로 입력된 프로그래밍 언어의 전신입니다.그것은 귀납적 패밀리와 의존적 패턴 [1][2]매칭을 지원하는 최초의 언어였다.
레퍼런스
- ^ 티에리 코캉(1992)"Dependent Types에서의 패턴 매칭"Bengt Nordström, Kent Petersson 및 Gordon Plotkin(편집자)에서 논리적 프레임워크에 관한 제3회 연례 BRA 워크숍의 전자 의사록(스웨덴 보스타드).
- ^ 토르스텐 알텐커치, 코너 맥브라이드, 제임스 맥키나(2005)."의존 유형이 중요한 이유"
읽고 추가
- 레나 마그누손과 벵트 노르드스트롬."ALF 교정 에디터와 그 교정 엔진"
- 토르스텐 알텐키르흐, 베로니카 가스페스, 벵트 노르드스트롬, 비욘 폰 시드."ALF 사용자 가이드"
