-
SIGPL Winter School 2017 3일차 정리
SIGPL Winter School 2017 3일차 정리 마지막 날 Type Check Val/Computation.Inductive/Fuction 4가지 룰이랑 Eval만 사용해서 체크함 logical한 step 4개의 룰만 있으면 거의 모든 증명을 할 수 있음 나머지 불가능한 것도 axiom? 추가하면 가능 프로그램 식을 그대로 읽으면 증명하는 거랑 똑같음 ->은 non dependent function forall은 dependent function ==forall, ->, =, P -> false, True, False, /|, |/, exists== 이것만 가지고 모든 set을 만들 수 있음 set이 바로 proposition (coq에서, m zigler set은 set prop는 prop)...
-
SIGPL Winter School 2017 2일차 정리
SIGPL Winter School 2017 2일차 정리 Martin Ziegler Logic 강의 tautology - always true satisfiability - true but not always inconsistency - false emptyset : false -> true 추후에 추가 예정 다시 Coq 강의 istrue = predicate type check 동시에 evaluate P -> Q P ------------ Q 증명 불가능한 함수는 짤 수 없다 1+(n:nat)를 짤 수는 없지만 1+(n:nat)->false 는 가능 evaluation은 증명을 단순화 시키는 것, simplify type checking 할 때 evaluation 해도 안전함 eval termination...
-
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에 참여하여 보고, 듣고, 배우고, 느낀점을 정리한 글입니다. 관련 자료가 여기(슬라이드)와 여기(책) 있으니 필요하신 분은 참고하시기 바랍니다!