Nyan101 Blog

Introduction 여기서는 Coq에서 사용되는 Galina라는 functional programming language의 기초적인 사용법과, Coq에서 증명에 실제 활용되는 기초적인 tactic에 대해 다룬다. Data and Functions Days of the Week 먼저 Coq에서 타입을 선언하는 법을 알아보자. 모든 Coq 구문은 .(마침표)로 끝남에 유의하자 Inductive day : Type := | monday | tuesday | wednesday | thursday...

Coq를 공부해보겠다는 막연한 목표와 함께 이런저런 자료를 찾아보고 그만두기를 반복하던 중, DeepSpec Summer School 세미나에서 나온 영상을 발견했다. 유투브에서 찾은 다른 영상들이 4,5년 전 자료였던 반면 DeepSpec에서는 최근인 2017, 2018년까지 꾸준히 학습자료와 세미나 영상이 업로드되고 있다. 사실 예전 LaTeX을 익힐 때에도 이것저것 찾아보기만 하다가 결국 학교 과제를 LaTeX으로 작성해보고서야 익숙해졌는데,...

동아리 톡방에서 이데일리 코딩대회에 대한 소식을 들었다. 학부를 졸업했지만 아직 대학원생은 아니라는 애매한 신분 때문에 대부분의 대회를 참가하지 못했었는데, 이번 대회는 청소년부/성인부로만 나뉘어져 있어 참가신청을 할 수 있었다. 예선 10월 26일 온라인 예선이 다가오자 안내문자가 날아왔는데, 처음엔 눈을 의심했다. 48시간 대회라는 점도 특이했지만 120문제라는 엄청난 문제 수에선 말이 나오지 않았다....

어째 코드잼 관련 글만 계속 올라오는 것 같다.. 여튼 이틀 전 Code Jam Kickstart Round G가 있길래 참가했다. 일요일 오후 10시라는 시간대가 조금 걸렸지만 월요일 연차휴가라는 사실에 힘입어 대회를 치르기로 했다. 대회 초반에 빠르게 문제를 풀고 중간 등수가 6등까지 올라갔다. 남은 1시간 반 동안 C 라지를 마저 풀까 하다가 exponential...

TL;DR : 로컬의 문제점을 깨닫지 못하고 폭사(…) 페이스북 해커컵이 끝났다. 구글 코드잼 본대회는 대회 당시 인터넷을 쓸 수 없는 환경(…)에 있어서 아쉬운 마음이었는데, 다행히 해커컵은 일정이 맞아 모두 참가할 수 있었다. 생각치 못한 실수로 Round 2에서 탈락했지만 각 라운드를 간단히 요약해봤다. Qualification Round 당시 아직 ‘전직’을 한 상태가 아니었지만 주말이라...

공식적으로 전직(…)을 했지만 가능한 한 PS대회는 계속 나가보고 싶었다. SCPC나 UCPC는 이제 대학생이 아니라 참가를 못했지만, 지난 주말에 Code Jam Kickstart Round D가 있어 여기 참가해볼 수 있었다. 코드잼 킥스타트에 대한 설명은 Round C 후기에서 한번 작성한 바 있으니 이 글에서는 생략했다. 이날 대회는 오후 2시부터 열렸는데, 내가 3시부터 세미나가...

한동안 개인 사정으로 인해 다른 일을 할 수 없어 Google Code Jam 본대회 Qualification Round를 불참했는데, 마침 오늘 Code Jam Kickstart 가 있길래 참가해봤다. Kickstart는 CodeJam 본대회와 달리 비교적 자주 진행되고(2017년 기준 7회), 다양한 시간대에 분포해 있어 코포처럼 새벽까지 깨어있지 않아도 참가할 수 있다. 대회 자체적으로 상을 주지는 않지만 좋은...

대부분의 reference가 그렇듯이 읽다보면 쉽게 지루해진다. 지루함을 덜하고 Coq에 익숙해지기 위해 일단 예제를 조금씩 따라해보면서 익혀가기로 했다. 자바를 처음 배울 때 public static void main(int argv, char **argc)가 정확히 뭔지는 몰라도 “Hello World” 부터 찍어보는 그런 마음으로 진행해봤다. CoqIDE 실행 프로그램을 처음 실행하면 다음과 같은 화면을 볼 수 있다. 크게...

<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만원)을 받아갈 수 있었다. 개인별로 사진과 같은 환경이 제공되었고 저기서 노트북이랑 책상 빼고는 전부 집으로 가져갈 수 있었다....