Efficient Logical Frameworks

高效的逻辑框架

• 批准号: 0306313
• 负责人: Frank Pfenning
• 金额: $ 31.87万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2003
• 资助国家: 美国
• 起止时间: 2003-07-01 至 2007-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0306313&HistoricalAwards=false
• 关键词: Efficient; Logical; Frameworks; 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.

逻辑框架是在机器支持的情况下正式指定逻辑和推理的语言。 示例是证明程序安全或验证受保护数据的访问权利的逻辑。该项目研究了逻辑框架的理论基础和有效的实施技术。 具体而言，该项目解决了Twelf逻辑框架的当前大规模应用中的性能瓶颈，旨在改善国家网络基础架构中移动代码的安全性和安全性。这些技术包括基于固有冗余性的证明压缩的方法，以及增加证明搜索和验证中自动化程度的方法。Logic是计算机科学中的关键学科，因为它允许我们允许我们做出“是的，此程序，可以安全地运行”或“是的，是的，允许该代理可以访问这些数据”。 关键的概念是正式的证明，它可以说服代码接收者的安全性或访问权限操作系统。 逻辑框架代表诸如数据结构之类的证据。 该项目研究了有效操纵这些数据结构的方法，以便它们可以用于现实的大规模应用中。 该系统还用于教授本科生在计算机科学和数学中应用的正式逻辑概念。