EAGER: Exploration in Type Systems With User-Defined Axioms

这个探索性项目的目的是用用户定义的公理对实际编程进行研究，以探索如何在结构化泛型编程中利用通过公理表达的语义信息。这项工作是研究可靠、可扩展的泛型编程并将其应用于科学软件的初步步骤。更具体地说，PI将调查如何以及哪些形式的用户定义公理可以转变为补充传统类型系统的属性决策程序。这项工作的目标是C编程语言，它拥有庞大的代码和程序员基础，因此将产生广泛的影响。这项工作将解决如何使用公理使程序更简单、更灵活并为代码生成器提供语义信息的问题。该系统将作为开源软件发布，并在计算机代数软件上进行评估。

The aim of this exploratory project is to conduct a study of practical programming with user-defined axiom to explore how semantic information, expressed through axioms, can be taken advantage of in structured generic programming. This work is a preliminary step to doing research on dependable, scalable generic programming, with application to scientific software. More specifically, the PI will investigate how, and which forms of user-defined axioms can be turned into property decision procedures that complement conventional type systems. This target of this work is the C++ programming language, which has a huge base of code and programmers and thus will have a broad impact. The work will address the question of how axioms can be used to make programs simpler, more flexible, and provide semantic information to code generators. The system will be released as open source software and evaluated on software from computer algebra.