학술활동


[초청세미나] 2016년 학과 콜로키움 시리즈 #0 - 안기영 박사

작성자
컴퓨터공학과
작성일
2016-01-06 17:42
조회
2166
제목: 논리 프로그래밍을 이용한 다형 타입 시스템의 실행 가능한 관계형 명세
강사: 안기영 (http://kyagrd.github.io/)
일시: 2016년 1월 8일 오전 11-12시
장소: 제3공학관 315호

개요


논리 프로그래밍 언어를 이용하면 컴퓨터로 실행 가능한 Hindley--Milner 타입 시스템(HM)의 선언적 명세가 가능하다. 현대적인 함수형 언어 구현들의 경우, 예컨대 GHC등에서는 HM보다 더 진보한 형태의 다형성을 지원한다. 이번 발표에서는 프롤로그로 작성한 HM의 명세로부터 시작해 더 많은 기능을 지원하도록 점진적으로 타입 시스템의 명세를 확장해 나가는 과정을 보여준다. 이 과정을 통해 얻은 교훈을 돌아보고 앞으로 이 아이디어를 기반으로 더 실용적인 언어 디자인/개발 도구 만들어 나가기 위한 TIPER(http://kyagrd.github.io/tiper/) 프로젝트의 계획과 진행 상황도
소개한다.


발표자: 안기영 박사는 미국 여러 대학의 교수님들(T. Sheard, A. Stump, S. Weirich)이 공동으로 차세대 의존 타입 언어 연구를 목적으로 하는 Trellys 연구그룹에서 학위 과정을 수련했다. Nax언어의 이론과 설계/구현을 주제로 학위를 취득한 후 프로그래밍 언어 구현을 돕는 새로운 개념의 도구인 TIPER를 만들기 위한 프로젝트를 계획하여 진행중이다. TIPER는 타입 유추 엔진을 타입 시스템의 관계형 명세로부터 자동으로 생성함으로써, 마치 Lex/Yacc과 같은 도구가 문법분석을 자동화한 것처럼, 타입 시스템 구현을 자동화시키는 것을 목표로 하고 있다.

[English]
Title: Executable Relational Specifications of Polymorphic Type
Systems using Logic Programming
Speaker:  Ahn, Ki Yung (http://kyagrd.github.io/)
Time: 2016년 1월 8일 오전 11-12시
Place: 제3공학관 315호

Abstract


  A declarative and machine executable specification of the Hindley–Milner type system (HM) can be formulated using a logic programming language. Modern functional language implementations such as the GHC supports more advanced polymorphism beyond HM. We progressively extended the HM specification to include more features using Prolog. We will contemplate on the lessons from this case study and introduce the plans and progress of the TIPER project (http://kyagrd.github.io/tiper/) to push this idea further towards a more practical language design/implementation tool.


Bio : Ki Yung Ahn had his academic training participating in aninter-institutional Trellys research group (lead by T. Sheard, A. Stump, and S. Weirich) focused on the next generation dependently-typed languages. After his degree on the theory, design and implementation of the Nax language, Ki Yung is planning a project to build a new concept language construction tool called TIPER, which will automatically generate Type Inference Prototyping Engings from
Relational specifications, visioning TIPER to be the tool for type systems as Lex/Yacc is for parser.