A Higher-Order Abstract Syntax Approach to Reasoning about Programs and Programming Languages

推理程序和编程语言的高阶抽象语法方法

• 批准号: RGPIN-2015-04158
• 负责人: Felty, Amy
• 金额: $ 3.13万
• 依托单位: University of Ottawa
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2015
• 资助国家: 加拿大
• 起止时间: 2015-01-01 至 2016-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=589630
• 关键词: Higher; Order; Abstract; Syntax; Approach

The principle objective of the proposed research is to advance the state of the art in techniques for proving properties of programs and programming languages. The proposed work falls within the area of formal methods and focuses on formal proof, which has the potential to provide an exceptionally high level of assurance that desired properties of software systems (such as safety, privacy, security, and correctness) hold. Application areas for this work include developing more secure programming languages, more robust compilers, and more trustworthy software in general.

拟议研究的主要目标是提高证明程序和编程语言属性的技术的最新水平。 拟议的工作属于形式化方法领域，重点是形式化证明，它有可能为软件系统所需的属性（例如安全性、隐私性、安全性和正确性）提供极高水平的保证。 这项工作的应用领域包括开发更安全的编程语言、更强大的编译器和更值得信赖的软件。