서지주요정보
Proving FFMM type safety using coq = Coq을 이용한 FFMM의 타입 안전성 증명
서명 / 저자 Proving FFMM type safety using coq = Coq을 이용한 FFMM의 타입 안전성 증명 / Ji-Eung Kim.
저자명 Kim Ji-Eung ; 김지응
발행사항 [대전 : 한국과학기술원, 2011].
Online Access 원문보기 원문인쇄

소장정보

등록번호

8023172

소장위치/청구기호

학술문화관(문화관) 보존서고

MCS 11058

SMS전송

도서상태

이용가능

대출가능

반납예정일

초록정보

In this paper, we design a core calculus of the Fortress programming language, Featherweight Fortress with Multiple Dispatch and Multiple Inheritance (FFMM), which provides both multiple dispatch and multiple inheritance, and mechanize its type safety proof using COQ. Multiple dispatch allows method selection among overloaded methods at run time based on dynamic types of more than one method arguments, and multiple inheritance allows a type can have more than one super types. Both of them give high expressive power to programming languages. However, languages that provide multiple dispatch and multiple inheritance need static restrictions to prevent undefined method calls and ambiguous method calls at run time. While previous work proposed static restrictions to guarantee no undefined method calls and no ambiguous method calls at run time, they are not closely tied to a particular programing languages. Therefore, we devise a formal calculus that reflects static restrictions for safe multiple dispatch and multiple inheritance. On top of that, to rigorously show the type safety of our calculus, we mechanize the calculus and its type safety proof using COQ.

본 논문에서 우리는 Fortress 프로그래밍 언어의 작은 부분을 표현해준 언어임과 동시에 여러 함수 인자의 동적 정보를 참고한 실행 함수 할당 방식과 (multiple dispatch) 다중 상속을 (multiple inheritance) 포함하고 있는 언어인 Featherweight Fortress with Multiple Dispatch and Multiple Inheritance, 즉 FFMM을 설계하였고, 또한 이 언어의 타입 안전성 증명을 COQ을 이용하여 구현하였다. 여러 함수 인자의 동적 정보를 참고한 실행 함수 할당 방식은 프로그램이 실행되는 시기에 여러 개의 동일한 이름을 가진 함수들 중 실제로 실행할 함수를 선택하는 데 있어서 여러 함수 인자들의 실행 시간 타입 정보를 이용하는 방식을 의미하며, 다중상속은하나의타입이여러개의부모타입을가질수있다는것을의미한다. 이 두 가지 개념은 프로그래밍 언어가 높은 표현력을 가질 수 있도록 도와준다. 하지만, 여러 함수 인자를 참고한 실행 함수 할당 방식과 다중 상속을 지원하는 언어들은 실행 시간에 수행되는 함수 호출에 있어서 호출 할 함수가 없는 경우나 (undefined method calls) 여러 개의 함수들 중 어떠한 함수를 호출해야 할 지 고르기 애매한 경우를 (ambigous method calls) 막기 위하여 정적인 제한 사항들을 필요로 한다. 기존에 실행 시간에 호출할 함수가 없는 경우와 어떠한 함수를 호출해야 할 지 고르기 애매한 경우가 일어나지 않는다는 것을 보장하는 정적인 제약 사항들을 제안한 연구가 있었지만, 그 제약 사항들은 특정한 언어와 밀접하게 연관이 있지는 않았다. 따라서,우리는여러함수인자의동적정보를참고한실행함수할당방식과다중상속을 안전하게 언어에 포함 시키기 위하여 필요한 정적인 제약 사항들을 반영하고 있는 언어를 고안하였으며, 또한 이 언어가 타입 안전성을 만족한다는 것을 엄밀히 보여주기 위하여 우리는 이 언어와 언어의 타입 안전성 증명을 COQ을 사용하여 구현하였다.

서지기타정보

서지기타정보
청구기호 {MCS 11058
형태사항 v, 31 p. : 삽도 ; 30 cm
언어 영어
일반주기 저자명의 한글표기 : 김지응
지도교수의 영문표기 : Suk-Young Ryu
지도교수의 한글표기 : 류석영
학위논문 학위논문(석사) - 한국과학기술원 : 전산학과,
서지주기 References : p.26-28
주제 Coq
Fortress
multiple dispatch
multiple inheritance
type system
Coq 증명 보조 도구
Fotress 프로그래밍 언어
여러 함수 인자의 동적 정보를 참고한 실행 함수 할당 방식
다중 상속
타입 시스템
QR CODE qr code