论文标题
逐渐键入的lambda calculi的参数化铸造和可重复使用的元理论
Parameterized Cast Calculi and Reusable Meta-theory for Gradually Typed Lambda Calculi
论文作者
论文摘要
对逐渐键入的研究导致了Siek and Taha（2006）及其基本的铸造微积分的逐渐键入Lambda演算（GTLC）的差异。例如，Wadler和Findler（2009）增加了责备跟踪，Siek等。 （2009年）研究了替代的演员评估策略，而Herman等人。 （2010年）用强制效率取代了铸件。 GTLC的元理论还扩大了超出类型安全性，包括责备安全性（Tobin-Hochstadt和Felleisen 2006），太空消费（Herman等，2010）和逐渐保证（Siek等人，2015年）。这些结果已被证明是GTLC的某些变化，但没有证明。此外，研究人员继续发展GTLC的差异，但是建立所有新变化的元理论是耗时的。 本文确定了以两个参数化的铸造表的形式捕获许多铸造微积分之间相似之处的抽象，一个是为了语言规范，另一个是指导空间效率的实现。然后，该文章为这两个微积分开发了可重复使用的元理论，证明了类型的安全性，责备安全性，渐进的保证和太空消耗。最后，该文章对八个演员表进行了实例化此元理论，其中包括文献中的五种和三个新的微积分。所有这些定义和定理，包括两个参数化的计算，可重复使用的元理论和八个实例化，在AGDA方面进行了机械化，从而大量使用模块参数和依赖记录来定义抽象。
The research on gradual typing has led to many variations on the Gradually Typed Lambda Calculus (GTLC) of Siek and Taha (2006) and its underlying cast calculus. For example, Wadler and Findler (2009) added blame tracking, Siek et al. (2009) investigated alternate cast evaluation strategies, and Herman et al. (2010) replaced casts with coercions for space-efficiency. The meta-theory for the GTLC has also expanded beyond type safety to include blame safety (Tobin-Hochstadt and Felleisen 2006), space consumption (Herman et al. 2010), and the gradual guarantees (Siek et al. 2015). These results have been proven for some variations of the GTLC but not others. Furthermore, researchers continue to develop variations on the GTLC but establishing all of the meta-theory for new variations is time consuming. This article identifies abstractions that capture similarities between many cast calculi in the form of two parameterized cast calculi, one for the purposes of language specification and the other to guide space-efficient implementations. The article then develops reusable meta-theory for these two calculi, proving type safety, blame safety, the gradual guarantees, and space consumption. Finally, the article instantiates this meta-theory for eight cast calculi including five from the literature and three new calculi. All of these definitions and theorems, including the two parameterized calculi, the reusable meta-theory, and the eight instantiations, are mechanized in Agda making extensive use of module parameters and dependent records to define the abstractions.
