• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >A type system for certified runtime type analysis.
【24h】

A type system for certified runtime type analysis.

机译：用于认证的运行时类型分析的类型系统。

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Modern programming paradigms are increasingly giving rise to applications that require type information at runtime. For example, services like garbage collection, marshalling, and serialization need to analyze type information at runtime. When compiling code which uses runtime type inspections, most existing compilers use untyped intermediate languages and discard type information at an early stage. Unfortunately, such an approach is incompatible with type-based certifying compilation.; A certifying compiler generates not only the code but also a proof that the code obeys a security policy. Therefore, one need not trust the correctness of a compiler generating certified code, instead one can verify the correctness of the generated code. This allows a code consumer to accept code from untrusted sources which is specially advantageous in a networked environment. In practice, most certifying compilers use a type system for generating and encoding the proofs. These systems are called type-based certifying compilers.; This dissertation describes a type system that can be used for supporting runtime type analysis in type-based certifying compilers. The type system has two novel features.; First, type analysis can be applied to the type of any runtime value. In particular quantified types such as polymorphic and existential types can also be analyzed, yet type-checking remains decidable. This allows the system to be used for applications such as a copying garbage collector. Type analysis plays the key role in formalizing the contract between the mutator and the collector, and also in the construction of different type-safe garbage collectors.; Second, the system integrates runtime type analysis with the explicit representation of proofs and propositions. Essentially, it integrates an entire proof language into the type system for a compiler intermediate language. Existing certifying compilers have focussed only on simple memory and control-flow safety. This system can be used for certifying more advanced properties while still retaining decidable type-checking.
机译：现代编程范例越来越多地导致在运行时需要类型信息的应用程序。例如，诸如垃圾收集，编组和序列化之类的服务需要在运行时分析类型信息。在编译使用运行时类型检查的代码时，大多数现有的编译器使用无类型的中间语言并在早期阶段丢弃类型信息。不幸的是，这种方法与基于类型的证明编译不兼容。认证编译器不仅会生成代码，还会生成证明代码遵守安全策略的证明。因此，人们不必相信生成认证代码的编译器的正确性，而是可以验证所生成代码的正确性。这允许代码使用者接受来自不受信任来源的代码，这在网络环境中特别有利。实际上，大多数认证编译器都使用类型系统来生成和编码证明。这些系统称为基于类型的证明编译器。本文描述了一种类型系统，该类型系统可用于支持基于类型的认证编译器中的运行时类型分析。类型系统具有两个新颖的特征。首先，类型分析可以应用于任何运行时值的类型。特别地，还可以分析量化类型，例如多态和存在类型，但是类型检查仍然是可确定的。这允许该系统用于诸如复制垃圾收集器之类的应用程序。类型分析在形式化转换器和收集器之间的契约以及构建不同类型安全的垃圾收集器中起着关键作用。其次，系统将运行时类型分析与证明和命题的显式表示相集成。本质上，它将整个证明语言集成到用于编译器中间语言的类型系统中。现有的认证编译器仅专注于简单的内存和控制流安全性。该系统可用于认证更高级的属性，同时仍保留可确定的类型检查。

著录项

  • 作者

    Saha, Bratin.;

  • 作者单位

    Yale University.;

  • 授予单位 Yale University.;
  • 学科 Computer Science.
  • 学位 Ph.D.
  • 年度 2002
  • 页码 211 p.
  • 总页数 211
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类 自动化技术、计算机技术;
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号