Strongly bounded termination with applications to security and hardware synthesis
Strongly bounded termination with applications to security and hardware synthesis
复制标题
强有界终止与安全和硬件综合应用
DOI：
10.1145/3406089.3409029
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Allwein, Gerard
中科院分区：
文献类型：
--
作者：
Reynolds, Thomas;Harrison, William L.;Chadha, Rohit;Allwein, Gerard
终止性检查是一种经典的静态分析，并且，在此焦点内，存在将终止性分析形式化为类型系统的基于类型的方法（即，所以所有类型良好的程序都终止）。但是在某些情况下，必须确定一个更强的终止性质（我们称之为强有界终止），因此，我们通过简单类型λ-演算的一个变体来探索这个性质，称为有界时间λ-演算（BTC）。本文介绍了BTC及其语义和元理论，通过Coq形式化。重要的例子（例如，从功能语言和隐蔽定时通道的检测硬件合成）激励强有界终止和BTC也被描述。
Termination checking is a classic static analysis, and, within this focus, there are type-based approaches that formalize termination analysis as type systems (i.e., so that all well-typed programs terminate). But there are situations where a stronger termination property (which we call strongly-bounded termination) must be determined and, accordingly, we explore this property via a variant of the simply-typed λ-calculus called the bounded-time λ-calculus (BTC). This paper presents the BTC and its semantics and metatheory through a Coq formalization. Important examples (e.g., hardware synthesis from functional languages and detection of covert timing channels) motivating strongly-bounded termination and BTC are described as well.
登录
查看更多内容
类型论中的结构递归定义
DOI：
--
发表时间：
1998
期刊：
International Colloquium on Automata, Languages and Programming
影响因子：
--
作者：
Eduardo Giménez
通讯作者：
Eduardo Giménez
关于归纳结构演算中基于类型的终止和依赖模式匹配。
DOI：
--
发表时间：
2011
期刊：
影响因子：
--
作者：
J. Sacchini
通讯作者：
J. Sacchini
类型理论中的无限对象
DOI：
--
发表时间：
1986
期刊：
Logic in Computer Science
影响因子：
--
作者：
N. Mendler;P. Panangaden;R. Constable
通讯作者：
R. Constable
具有尺寸产品的基于类型的端接
DOI：
--
发表时间：
2008
期刊：
Annual Conference for Computer Science Logic
影响因子：
--
作者：
G. Barthe;B. Grégoire;Colin Riba
通讯作者：
Colin Riba
资源半环中的有界线性类型
DOI：
--
发表时间：
2014
期刊：
European Symposium on Programming
影响因子：
--
作者：
D. Ghica;Alex I. Smith
通讯作者：
Alex I. Smith