-
SIGPL Winter School 2017 1일차 정리
SIGPL Winter School 2017 1일차 정리 주어가 명시되지 않은 문장은 대부분 Coq가 그렇다는 의미로 받아들이면 대부분 알아들을 수 있을 것이다. Coq는 실제 계산할 때 퍼포먼스 때문에 nat에서 다른 타입으로 계산을 허용한다고 한다. Coq로 짠 코드를 실행하다가 오버플로우 등의 현실적인 에러가 발생할 수 있지만, 애초에 Coq는 Theorem을 증명하는 데에 목적을 두기 때문에 Coq에 대해 문제를 제기할 필요는 없다. 문제 없이 Type Check를 통과하면 안전하다고 보장된다. 이의를 제기할 필요는 없다. Type Check를 통과하면 안전하다는 사실이 이미 다...
-
SIGPL Winter School 2017
SIGPL Winter School 2017 SIGPL Winter School 2017에 참여하여 보고, 듣고, 배우고, 느낀점을 정리한 글입니다. 관련 자료가 여기(슬라이드)와 여기(책) 있으니 필요하신 분은 참고하시기 바랍니다!