Dependent Types for Low-Level Programming
Dependent Types for Low-Level Programming
复制标题
低级编程的依赖类型
DOI：
10.1007/978-3-540-71316-6_35
复制
发表时间：
2007
影响因子：
3.2
通讯作者：
G. Necula
中科院分区：
文献类型：
--
作者：
Jeremy Condit;M. Harren;Zachary R. Anderson;David E. Gay;G. Necula
在本文中，我们描述了低级命令式语言的依赖类型系统的关键原理。这项工作的主要贡献是（1）一个健全的类型系统，它以比以前更灵活的方式结合了变量和堆分配结构的依赖类型和突变，以及（2）自动推断局部变量的依赖类型的技术。我们应用这些一般原则来设计 Vice，这是一个 C 的依赖类型系统，允许用户描述有界指针和标记联合。 Vice 已被用来注释和检查许多现实世界的 C 程序。
In this paper, we describe the key principles of a dependent type system for low-level imperative languages. The major contributions of this work are (1) a sound type system that combines dependent types and mutation for variables and for heap-allocated structures in a more flexible way than before and (2) a technique for automatically inferring dependent types for local variables. We have applied these general principles to design Deputy, a dependent type system for C that allows the user to describe bounded pointers and tagged unions. Deputy has been used to annotate and check a number of real-world C programs.