文章基本信息

标题：Towards Strong Normalization for Dependent Object Types (DOT)
本地全文：下载
作者：Fei Wang ; Tiark Rompf
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：74
页码：27:1-27:25
DOI：10.4230/LIPIcs.ECOOP.2017.27
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar languages, unifying functional programming, object oriented programming and ML-style module systems. Following the recent type soundness proof for DOT, the present paper aims to establish stronger meta-theoretic properties. The main result is a fully mechanized proof of strong normalization for D_<:, a variant of DOT that excludes recursive functions and recursive types. We further discuss techniques and challenges for adding recursive types while maintaining strong normalization, and demonstrate that certain variants of recursive self types can be integrated successfully.
关键词：Scala; DOT; strong normalization; logical relations; recursive types