Bidirectional type checking for relational properties
Bidirectional type checking for relational properties
复制标题
关系属性的双向类型检查
DOI：
10.1145/3314221.3314603
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Garg, Deepak
中科院分区：
文献类型：
--
作者：
Çiçek, Ezgi;Qu, Weihao;Barthe, Gilles;Gaboardi, Marco;Garg, Deepak
关系型系统已被设计用于多种应用，包括信息流、差异隐私和成本分析。为了达到最好的结果，这些系统经常使用关系求精和关系效果来最大限度地利用被比较的两个程序结构上的相似性。关系类型系统对关系属性很有吸引力，因为它们提供了比分别键入两个程序所获得的验证更简单、更精确的验证。然而，关系类型系统还没有达到非关系类型系统的实际吸引力，部分原因是缺乏实现它们的一般基础。在本文中，我们通过为具有关系精化和效果的系统开发双向关系类型检查来朝着这个方向迈出一步。我们的方法在关系环境中实现了双向类型检查的好处。特别是，它通过类型检查和类型推断的组合显著减少了键入批注的需要。为了突出我们方法的基本性质，我们开发了几个关系类型系统的双向版本，这些系统增量地组合了表达式关系分析所需的许多不同组件。
Relational type systems have been designed for several applications including information flow, differential privacy, and cost analysis. In order to achieve the best results, these systems often use relational refinements and relational effects to maximally exploit the similarity in the structure of the two programs being compared. Relational type systems are appealing for relational properties because they deliver simpler and more precise verification than what could be derived from typing the two programs separately. However, relational type systems do not yet achieve the practical appeal of their non-relational counterpart, in part because of the lack of a general foundation for implementing them.In this paper, we take a step in this direction by developing bidirectional relational type checking for systems with relational refinements and effects. Our approach achieves the benefits of bidirectional type checking, in a relational setting. In particular, it significantly reduces the need for typing annotations through the combination of type checking and type inference. In order to highlight the foundational nature of our approach, we develop bidirectional versions of several relational type systems which incrementally combine many different components needed for expressive relational analysis.
登录
查看更多内容
类型推断、Haskell 和依赖类型
DOI：
--
发表时间：
2013
期刊：
影响因子：
--
作者：
Adam Gundry
通讯作者：
Adam Gundry
随控制流变化而增加计算复杂性的类型理论
DOI：
--
发表时间：
2016
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Ezgi Çiçek;Zoe Paraskevopoulou;D. Garg
通讯作者：
D. Garg
继承作为隐式强制
影响因子：
1
作者：
V. Tannen;T. Coquand;Carl A. Gunter;A. Scedrov
通讯作者：
A. Scedrov
LiquidHaskell
DOI：
--
发表时间：
2014
期刊：
ACM SIGPLAN Symposium/Workshop on Haskell
影响因子：
--
作者：
Niki Vazou;Eric L. Seidel;Ranjit Jhala
通讯作者：
Ranjit Jhala
线性相关类型和相对完整性
DOI：
10.2168/lmcs-8(4:11)2012
发表时间：
2011
期刊：
2011 IEEE 26th Annual Symposium on Logic in Computer Science
影响因子：
--
作者：
Ugo Dal Lago;Marco Gaboardi
通讯作者：
Marco Gaboardi