渐进类型系统能在同一个程序语言中融合静态类型和动态类型，不仅能保证程序的安全可靠性，而且也能提高编程的效率和灵活性。渐进类型系统是当前程序语言方面的一大研究热点，且已开始被纳入到基于语言安全的技术中，即渐进安全类型系统。然而，目前关于渐进安全类型系统的研究处于起步阶段，很多问题亟待解决。为此，本项目拟对渐进安全类型系统展开研究，构建面向不同抽象级别语言的渐进安全类型系统，以及设计基于渐进类型的不同抽象级别上的语言之间的转化。项目的研究重点在于（1）定义支持依赖类型的渐进安全类型系统；（2）设计高效可靠的类型检测算法和类型推导算法；(3）构建面向低级语言的渐进安全类型系统；（4）研究渐进类型系统在不同抽象层次的语言间的转化的属性，包括类型保持、张度和渐进保证。项目的研究，不仅有望进一步丰富渐进类型的理论研究，而且对基于语言安全的研究有积极意义。

A gradual type system integrates static and dynamic typing in a single programming language. It can not only guarantee the safety and reliability of programs, but can also improve the efficiency and flexibility of programming. Gradual typing has become one of the research highlights in programming languages, and thus has been used in language-base security, namely, gradual security type systems. However, the state-of-the-art research in this area is still very much in its infancy, with a lot of open challenges. To tackle some of the challenges, this project aims to construct gradual security type systems for different abstract level languages, and propose the translation based on gradual typing between languages of different abstract levels. In this project, we will (1) define a gradual security type system with dependent types; (2) design the efficient and sound type checking algorithms and type inference algorithms; (3) construct a gradual security type system for low-level languages; (4) study the properties of the translation between languages of different abstract levels, including type preservation, tension and gradual guarantee. This work not only can enrich the theoretical study on gradual typing, but also has a positive meaning for language-based security.