나는 agda를 배우려고 노력하고있다. 그러나 문제가 있습니다. agda wiki에서 찾은 모든 자습서는 나에게 너무 복잡하고 프로그래밍의 다양한 측면을 다룹니다. agda에 대한 3 가지 자습서를 병렬로 읽은 후에 간단한 교정본을 작성할 수 있었지만 실제 단어 알고리즘의 정확성을 위해 충분한 지식을 가지고 있지 않습니다.agda 배우는 방법
주제에 대한 자습서를 추천 해 주시겠습니까? 하스켈을 배우는 것과 비슷한, Agda를위한 것.
약 1 년 전에 Agda를 배우기 시작했을 때 나는 가능한 모든 튜토리얼을 시도했고 각각 새로운 것을 가르쳐 주었다고 생각합니다. 그것은 더 큰 사용자 기반을 가지고 있으며,이 좋은 대해 사용 가능한 책이 있기 때문에
당신은 아마, COQ에게 시험을 주어야한다 :
Software Foundations도 매우 좋습니다.
좋은 점은 Agda와 Coq의 이론이 다소 비슷하다는 점입니다. 따라서 많은 예제가 서로 변환 될 수 있습니다. Programming in Martin-Löf's Type Theory은 종속 형식 이론에 대한 정말 훌륭하고 읽기 쉬운 소개이며, 당신을 위해 몇 가지를 정리할 수 있습니다.
"실제 알고리즘"이 무슨 뜻인지 아는 것이 도움이 될 것입니다. 많은 예제 개발은 papers which mention Agda에 설명되어 있습니다.
작년에 Conda McBride는 Agda를 사용한 의존형 프로그래밍을 통해 a great series of lectures을주었습니다. 주제에 대한 간략한 튜토리얼을 통해 휴식을 취하고 싶다면 이동하는 것이 좋습니다. 나는 또한 수반되는 운동이 있다고 믿는다.
관련 질문 (질문하기) : http://stackoverflow.com/questions/13497865/where-to-start-with-dependent-type-programming/14292455#14292455 –
Agda는 아니지만 Idris는 아니지만 여전히 상당히 관련이 있습니다. https://vimeo.com/117221082 –