한국정보과학회 프로그래밍언어연구회 여름학교
(SIGPL Summer School 2009)

  • 주제: Coq를 이용한 정리증명 및 프로그래밍
  • 일시: 2009년 8월 18일(화) ~ 8월 20일(목)
  • 장소: 목포대학교 도림캠퍼스 대외협력관 1층 소강의실

  • 한국정보과학회 프로그래밍언어 연구회(SIGPL)는 매년 여름과 겨울 방학기간에 대학원생과 엔지니어, 교수, 연구자들을 대상으로 계절학교를 개최하고 있습니다. 이번 여름학교에서는 정형 증명 도구 Coq를 이용하여 논리학의 정리 증명 이론을 프로그래밍하고 실습하는 강의를 준비하였습니다. 프로그래밍언어, 정형 기법, 시스템의 검증과 안전성, 그리고 전산학의 기초 이론 분야에 유익한 기회가 될 수 있을 것입니다. 많은 관심과 참여를 부탁드립니다.

    한국정보과학회 프로그래밍언어연구회 운영위원장 변석우

    프로그램 소개

    SIGPL 2009 여름학교에서는 증명보조기 Coq을 이용한 프로그래밍에 대해서 강좌를 개설합니다. 증명보조기 Coq을 이용해서 실제로 논리식으로 표현된 증명을 Coq 프로그램으로 표현하는 방법을 배우며, 기초적인 명제논리의 증명에서 시작하여 Coq 프로그래밍의 핵심 기법중의 하나인 귀납적 술어논리의 증명까지 다룹니다. 본 강좌는 이론적 배경을 설명하는 강의와 실제 Coq으로 프로그래밍을 해 보는 실습으로 구성되며, 실습시간에는 강사와 조교가 직접 프로그래밍을 도와주게 됩니다.

    본 강좌는 논리학에 관심이 있는 학부생, 대학원생을 주 대상으로 하며, 전산학의 기초 지식만 있으면 누구나 수강할 수 있도록 설계하였습니다.

    프로그램 일정

    첫째날 8월 18일 (화) 오후
    13:30 개교식
    14:00-15:20   class 1   natural deduction, propositional logic, proof term (강의)
    15:30-17:00 class 2 Coq 소개, propositional logic, proof term (강의, Coq 실습)
    17:30 만찬
    둘째날 8월 19일 (수) 오전
    09:00-10:20 class 3 first-order logic (강의, Coq 실습)
    10:30-12:00 class 4 inductive datatype, inductive predicate (강의)
    둘째날 8월 19일 (수) 오후
    13:00-14:20 class 5 inductive datatype (Coq 실습)
    14:30-16:00 class 6 inductive predicate (Coq 실습)
    셋째날 8월 20일 (목) 오전
    09:00-10:20 class 7 inductive proof (Coq 실습)
    10:30-12:00 class 8 inductive proof (Coq 실습)

    참가 준비

    참석하는 학생들은 실습을 위해서 노트북에 Coq 소프트웨어를 미리 설치해서 가져와야 합니다. (여름학교에서 노트북을 별도로 준비하지 않습니다.) Coq 소프트웨어는 다음 웹페이지에서 다운로드 받을 수 있으며 현재 웹페이지에서 제공되고 있는 8.2pl1 버전을 설치하면 됩니다. Coq 실습은 CoqIDE를 이용해서 진행하므로 CoqIDE가 실행되도록 준비하면 됩니다. Emacs 환경을 위한 CoqIDE 설치는 ProofGeneral을 이용하시면 됩니다.

    강의자료 및 숙제자료는 다음과 같습니다.

    등록안내

    준비위원회

    장소안내

    목포대학교 도림캠퍼스 오시는 길

    1. 승용차
    2. 기차 (KTX, 새마을, 무궁화) (KTX 용산역에서 3시간 20분)
    3. 버스 (강남역에서 약 4시간 30분)
    4. 비행기

    학교내부에서 대외협력관까지 오시는 길