17 citations · 17 across the 1 of their papers we have counts for
2 papers
cs.PL2015
A Verified Information-Flow Architecture
Arthur Azevedo de Amorim, Nathan Collins, André DeHon +6
SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supp…
cs.PL2012★ 17 cited
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn +7
We present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studi…