CRI: Machine Assistance for Programming Language Research

该项目旨在为机器检查程序设计语言(PL)研究论文编纂最佳实践，建议开发一本机器检查的教科书，介绍PL理论的基本结果。它还寻求为这类工作建立更好的库、验证策略和其他工具，并为社区打包它们。该基础设施汇集了一套全面的教育和技术资源，体现并推进了当前在对PLS研究的证明辅助支持方面的最佳实践，包括：-仔细研究并清楚地表述的一组用于编程语言工作的机器检查的最佳实践(包括对特定证明助理的选择和关于基本表示策略的一些关键决定)。-工具、定理库和针对一系列结构的证明自动化策略(例如具有变量绑定的句法、类型上下文、堆等)。这是一个网络可访问和社区可扩展的资源语料库，供研究人员和学生学习如何使他们自己的工作机械化，形式既有教程，也有说明一系列主题和技术的大规模、有良好记录和精美的例子。-一本关于PL的机器检验证明的综合教科书。这项工作位于PLS和定理证明的交叉点上，旨在扩展POPLMark挑战，以就PL类型系统中的各种问题的工具和代表性选择达成社区共识。广泛影响：编程语言形成了科学和社会日益依赖的软件系统的基础。这项研究促进了更好、更安全的编程语言；因此，潜在的影响必然是极其广泛和深刻的。技术成果可能会对国家关键计算基础设施的可信性产生积极影响。鼓励代表人数不足的人口参加讲习班，并确定资金为有需要的人提供学生奖学金。

This project, seeking to codify best practices for machine checking programming language (PL) research papers, proposes to develop a machine checked textbook of basic results in PL theory. It also seeks to build better libraries, proof tactics, and other tools for such work, and to package them for the community. The infrastructure, assembling a comprehensive set of educational and technological resources that embody and advance the current best practices in proof-assistant support for research in PLs, includes:-A carefully researched and clearly articulated set of best practices for machine checking of work in programming languages (including a choice of a particular proof assistant and some critical decisions about fundamental representation strategies).-Tools, libraries of theorems, and proof automation tactics for a range of structures (such as syntax with variable binding, typing contexts, heaps, etc.) commonly found in PL research.-A corpus of web-accessible and community-extensible resources for researchers and students to learn about how to mechanize their own work, in the form of both tutorials and large-scale, well-documented, and polished examples illustrating a range of topics and techniques. -An integrated textbook on machine checking proofs about PLs.This work, lying in the intersection of PLs and theorem proving, seeks to extend the POPLMark challenge to forge a community consensus on tools and representational choices for various problems in PL type systems.Broader Impact: Programming languages form the foundation for software systems on which science and society increasingly depend. This research promotes better and more secure programming languages; hence the potential impacts are bound to be extremely broad and deep. The technical results might have a positive impact on the trustworthiness of the national critical computing infrastructure. Underrepresented populations are encouraged to participate in workshops and funds are identified to provide student scholarships for the needy.