Efficient Logical Frameworks

逻辑框架是在机器支持下，用于指定逻辑和用它们进行形式化推理的语言。 例如，证明程序安全性或验证受保护数据的访问权限的逻辑。该项目研究逻辑框架的理论基础和有效的实现技术。 具体而言，该项目解决了目前大规模应用“数字化网络”逻辑框架的性能瓶颈问题，目的是提高国家网络基础设施内移动的代码的安全性。这些技术包括基于内在冗余的证明压缩方法，以及提高证明搜索和验证自动化程度的方法。逻辑是计算机科学中的一个关键学科，因为它允许我们做出明确的判断，例如“是的，这个程序可以安全运行”或“是的，这个代理可以访问这些数据”。 关键的概念是一个正式的证明，它可以说服代码接收者的安全性或访问权限的操作系统。 逻辑框架将这些证明表示为数据结构。 该项目研究有效操作这些数据结构的方法，以便它们可以用于实际的大规模应用程序。 正在建设中的系统也被用来教大学生形式逻辑的概念，因为它们被应用于计算机科学和数学。

Logical frameworks are languages for specifying logics and reasoning with them formally, with machine support. Examples are logics to prove the safety of programs or authenticate access rights to protected data. The project investigates theoretical foundations and efficient implementation techniques for logical frameworks. Specifically, the project addresses performance bottlenecks in current, large-scale applications of the Twelf logical framework aimed at improving safety and security of mobile code within the national cyber infrastructure. The techniques include methods for proof compression based on intrinsic redundancy, and methods to increase the degree of automation in proof search and verification.Logic is a key discipline in computer science because it allows us to make definitive judgments such as "yes, this program is safe to run" or "yes, this agent is allowed to access these data". The critical notion is that of a formal proof, which can convince a code recipient of its safety or an operating system of access rights. Logical frameworks represent such proofs as data structures. This project investigates methods to manipulate these data structures efficiently so they can be used in realistic, large-scale applications. The system under construction is also used to teach undergraduates the concepts of formal logic as they are applied in computer science and mathematics.