[질문] type theory 교과서 추천좀

[익명(39.7)]

그냥 coq이나 agda 책 읽으라는 사람도 있던데 그래도 레퍼런스 삼을만한 이론 교과서 하나 정도는 있으면 좋겠다 싶어서

수학과쪽 책도 괜찮으니까 명저다 싶은 거 있으면 추천좀 부탁드림다 연습문제 있으면 더 좋고

[다믜(damhiya)]

Coq, Agda는 Coq: [software foundations, certified programming with dependent types], Agda: [programming language foundations in agda]

[다믜(damhiya)]

다른건 Types and programming languages, Advanced topics in types and programming languages

[다믜(damhiya)]

TAPL은 실용적인 "프로그래밍 언어"의 타입시스템이 초점이라 ML 스타일 언어 타입 시스템의 구현 같은거 다룰거임. dependent type은 안나옴

[익명(39.7)]

감사함다 coq이나 agda 책이랑 아래 pierce 책이랑 병행해도 될까요 아님 보고 가는게 나을까요?

[다믜(damhiya)]

초점이 달라서 배우고 싶은게 정확히 뭔지에 따라 다를듯

[익명(39.7)]

감사합니다 일단 좀 보고 결정해야겠네요

[black7375(221.168)]

https://news.hada.io/topic?id=6572

[익명(39.7)]

감사합니다 엄청 깔끔하게 정리되어 있네요

[기괴공학도(thecoqproofassistant)]

dependent type theory 배우려는 거임?

[익명(39.7)]

넵 시간 넉넉히 잡고 hott까지 볼까 생각중입니다