An effective theory of type refinements

Special Interest Group on Programming Languages(2003)

引用 119|浏览73
摘要
We develop an explicit two level system that allows programmers to reason about the behavior of effectful programs. The first level is an ordinary ML-style type system, which confers standard properties on program behavior. The second level is a conservative extension of the first that uses a logic of type refinements to check more precise properties of program behavior. Our logic is a fragment of intuitionistic linear logic, which gives programmers the ability to reason locally about changes of program state. We provide a generic resource semantics for our logic as well as a sound, decidable, syntactic refinement-checking system. We also prove that refinements give rise to an optimization principle for programs. Finally, we illustrate the power of our system through a number of examples.
更多
查看译文
PDF
PPT

代码

数据

原文链接
引用

0
您的评分 :

暂无评分

标签
评论
avatar
作者解读

点赞

0%
0/20人

想看人数超过20人时,我们会邀请作者来解读:

  • 解决的问题
  • 实验设计的思路
  • 重要创新
  • 后续可能的深入研究
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn