Nyan101 Blog

<Interactive Theorem Proving and Program Development>라는 책을 추천받아 조금씩 읽어보기로 했다. 첫 장에서는 Coq에 대한 간단한 안내를 진행한다. 책의 순서를 따라가면서 하나씩 알아보자 타입 먼저 Coq에서는 Gallina라는 언어를 사용해 요구사항(Specification)을 서술한다. 대부분의 다른 프로그래밍 언어들과 마찬가지로 타입은 declaration과 typing rule에 의해 정해진다. declaration : type Z 에 대해 이 타입의...

지난 8월 17일 삼성전자 서울 R&D캠퍼스에서 열린 SCPC(Samsung Collegiate Programming Cup) 본선대회에 참가했다. 2015년 1회 대회부터 계속 본선까지만 진출하고 막상 수상은 못했어서 이번이 사실상 마지막 기회였는데, 졸업 전 마지막 대회라 운이 좋았는지 4등상(+200만원)을 받아갈 수 있었다. 개인별로 사진과 같은 환경이 제공되었고 저기서 노트북이랑 책상 빼고는 전부 집으로 가져갈 수 있었다....

이번 SCTF(Samsung CTF)의 700점짜리 문제로 튜링머신 설계가 나왔다. 총 4개의 문제 중 3개는 일반적인 오토마타 교과서에서 다루는 언어들(ex: \(L=\{ 0^n1^n | n \geq 0 \}\))이었지만 마지막 단계인 \(L=\{0^p | p \, \mathrm{\,is\,prime}\}\)가 다소 많은 시간을 잡아먹었다. 사실상 소수 판별을 하는 튜링 머신을 설계하라는 문제였는데, 기억상 다른 교재들에서도 이에 대한 명확한...

You’ll find this post in your _posts directory. Go ahead and edit it and re-build the site to see your changes. You can rebuild the site in many different ways, but the most common way is to run jekyll serve, which launches a web server and auto-regenerates your site when...