欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
编程语言类型系统的类型安全性可以保证程序运行时满足基本安全属性，包括控制流安全，内存安全等．类型化编程语言都需要一个类型检查器来检查程序的良类型性，因此编程语言的具体实现是否能保证类型安全性，还依赖类型检查器的可靠性．本文给出一种类型化汇编语言，然后给出相应的类型检查器，并证明了此类型检查器的可靠性，从而保证经过类型检查的汇编程序的安全性．文本的所有工作，包括类型化汇编语言、类型检查器以及相关定理证明，均已在证明辅助工具Coq中实现．本文方法也可用于证明类型化高级语言的类型检查器的可靠性．
英文摘要：
Typed programming languages guarantee the type safety of programs at runtime, such as control-flow safety and memory safety. A type checker is needed to check whether programs are well-typed. Therefore, the safety of a typed program- ming language still greatly depends on the soundness of its type checker. This paper proposes a typed assembly language with a type checker which is used to check the type of the programs written in this assembly language. Moreover, the soundness of the type checker has been proved so that we can ensure the type safety of any program passed through this certified type checker. All the work in this paper, including type system, type-checking algorithm and proofs, are formalized in the proof assistant Coq. The method proposed in this paper can also be applied to prove the soundness of type-checkers for higher-level typed programming languages.
同期刊论文项目
同项目期刊论文
期刊信息
位置：