SHF:Small:RUI: Semantic Complexity of Advanced Data Types

程序测试在过去50年的软件开发中占据主导地位，但未来50年将看到对可证明正确的软件的需求增加。这部分是因为现代应用程序越来越安全，部分是因为测试本质上只是部分正确性保证，部分是因为编程语言技术现在处于可以正式验证关键程序的阶段。基于数据库的验证使用编程语言的类型系统来帮助保证程序的正确性：类型系统可以表达的程序属性越多，编译器可以自动验证的属性就越多。高级数据类型（如广义代数数据类型（GADT））有助于缩小程序员对程序的了解与类型系统对这些程序的表达之间的所谓“语义鸿沟”。该项目的关键观察结果是，GADT和其他高级数据类型的语法未充分指定，这通常导致它们以不合理的方式使用，从而破坏了它们的验证承诺。该项目的新奇是对这一观察的完全语义响应，体现在数据类型的函子完成的全新概念中。这种函子补全的概念直接导致了项目的整体影响，即改变了程序员理解GADT和其他高级数据类型的方式，从而改变了程序员使用GADT和其他高级数据类型进行编程的方式。该项目表明，即使是普通的GADT目前的理解方式也是不合理的，并导致了不安全的编程实践，对软件系统的验证、安全性和可靠性产生了明显的后果。它给出了一种生成GADT和其他高级数据类型的非常通用的类的语法，并使用数据类型的函子完成的新概念来赋予由这种语法生成的数据类型相同的语义，这种语义长期以来一直是标准代数数据类型理论的基石。这确保了由语法生成的数据类型可以在语义和计算上有信心地使用。此外，它还允许根据语义复杂性对数据类型进行分类--这是本项目中引入的一个新概念--这有助于程序员更好地理解数据类型的语义和计算属性。最后，该项目给出了一个框架，用于为多态语言构建参数模型，支持由语法生成的高级数据类型。这个框架是原则性的，概念简单，统一，全面和预测。该奖项是专门为验证GADT的语义和由语法生成的其他高级数据类型，以及以标准方式从这些语义中派生的结构而设立的。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Testing of programs has dominated the last 50 years of software development, but the next 50 will see an increased demand for provably correct software. This is partly because modern applications are increasingly safety critical, partly because testing is by its very nature only a partial correctness guarantee, and partly because programming language technology is now at the stage where it is feasible to formally verify critical programs. Language-based verification uses a programming language's type system to help guarantee program correctness: the more program properties a type system can express, the more the compiler can automatically verify. Advanced data types such as Generalized Algebraic Data Types (GADTs) help close the so-called "semantic gap" between what programmers know about programs involving them and what a type system can express about those programs. The key observation underlying this project is that GADTs and other advanced data types are underspecified by their syntax, which often leads to them being used in unjustified ways that undermine their promise for verification. The project's novelty is a fully semantic response to this observation, embodied by the entirely novel notion of the functorial completion of a data type. This notion of functorial completion leads directly to the project's overall impact, which is to change the way programmers understand, and thus program with, GADTs and other advanced data types.The project shows that the way that even ordinary GADTs are currently understood is not formally justifiable and leads to unsafe programming practices, with the obvious consequences for verification, security, and reliability of software systems. It gives a grammar that generates a very general class of GADTs and other advanced data types, and uses the new notion of the functorial completion of a data type to give the data types generated by this grammar the same kind of semantics that has long been the cornerstone of the theory of standard algebraic data types. This ensures that data types generated by the grammar can be used with semantic and computational confidence. Furthermore it allows the data types to be classified according to semantic complexity--a novel notion introduced in this project--that helps programmers better understand a data type's semantic and computational properties. Finally, the project gives a framework for constructing parametric models for polymorphic languages supporting the advanced data types generated by the grammar. This framework is principled, conceptually simple, uniform, comprehensive, and predictive. It is constructed specifically to validate the semantics of the GADTs and other advanced data types generated by the grammar, and the constructs that are derived in a standard way from such semantics.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.