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을 사용하여 구현하였다.
