GTLC의 타입보존에 대한 기계증명 = Mechanized Proof for Type Preservation of GTLC

국문 초록 (Abstract)

동적 언어에서 정적 타입 검사의 장점을 필요에 따라 부분적으로 활용하기 위한 목적으로 점진적 타이핑이 현업에서 쓰이는 언어(예: Python, JavaScript 등)에도 활발히 도입되는 추세이며 그에 따라 점진타입 타입 시스템의 이론적 토대에 대한 엄밀한 연구의 필요성도 높아지고 있다. 본 논문에서는 점진적 타이핑을 포함하는 타입 시스템 중 가장 기초가 되는 점진적 타입 시스템 GTLC의 타입 안전성 증명의 일부인 타입보존 성질을 Abella 증명도우미를 이용해 기계증명으로 유도한 내용을 보고한다. 또 그 기계증명 내용 중 일부를 구체적으로 살펴보며 관련 연구에서 같은 내용을 다른 증명도우미로 기계증명한 것과 비교해 Abella로 점진적 타입 시스템을 형식화하고 기계증명하는 데 어떤 장단점이 있는지 분석한다.

다국어 초록 (Multilingual Abstract)

Over the past decade, there has been a growing trend of supporting selective use of static typing in dynamic languages, coined "gradual typing", among the major real-world programming languages (e.g., Python, JavaScript), motivating studies on the theoretical basis for gradual typing. We developed mechanized proof for subject reduction, which is one of the two key parts of the type safety property of the gradually typed lambda calculus(GTLC), using the Abella proof assistant. We further elaborate on some parts of our mechanized proofs in order to highlight the pros and cons of using Abella for developing mechanized theories on gradual typing, compared to prior related work on GTLC using other proof assistants.

참고문헌 (Reference)

1 A. Reid, "Trustworthy specifications of ARM®V8-A and V8-M system level architecture" FMCAD Inc 161-168, 2016

2 A. Gacek, "Relating nominal and higher-order abstract syntax specifications" ACM 177-186, 2010

3 J. G. Siek, "Refined Criteria for Gradual Typing" Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik 32 : 274-293, 2015

4 D. Ancona, "RPython: A step towards reconciling dynamically and statically typed OO languages" ACM 53-64, 2007

5 Y. Igarashi, "On polymorphic gradual typing" 1 : 40:1-40:29, 2017

6 D. Miller, "Higher-order logic programming" Springer 448-462, 1986

7 J. G. Siek, "Gradual typing for functional languages" University of Chicago 81-92, 2006

8 M. Toro, "Gradual parametricity, revisited" 3 : 17:1-V, 2019

9 L. D. Paulson, "Developers shift to dynamic programming languages" 40 : 12-15, 2007

10 J. Cheney, "Alpha-Prolog: A logic programming language with names, binding, and alpha-equivalence" Springer 3132 : 269-283, 2004

11 A. Gacek, "A two-level logic approach to reasoning about computations" 49 : 241-273, 2012

12 A. Church, "A formulation of the simple theory of types" 5 (5): 56-68, 1940

13 Hyeonseung Im, "A Brief Survey on Gradual Typing" KIISE 37 (37): 2019