可变 WadlerFest DOT 演算

依赖对象类型（DOT）演算旨在建模 Scala 的精髓，重点关注抽象类型成员、路径依赖类型和子类型。其他 Scala 特性可以通过转换为 DOT 来定义。可变性是 Scala 的一个基本特性，目前在 DOT 中缺失。DOT 中的可变性不仅需要对 Scala 程序中的副作用计算和可变性进行建模，甚至还需要精确指定 Scala 如何初始化不可变变量和字段（vals）。我们提出了 DOT 的一个扩展，增加了带类型的可变引用单元。我们已在 Coq 中通过机械化证明验证了该扩展的可靠性。我们展示了扩展演算的关键特性及其可靠性证明，并讨论了我们在寻找可靠设计过程中遇到的挑战以及我们考虑过的替代解决方案。