期刊论文详细信息
Brazilian Computer Society. Journal
Mechanized metatheory for a \(\lambda \) -calculus with trust types
article
Rodrigo Ribeiro1  Lucília Figueiredo2  Carlos Camarão1 
[1] Instituto de Ciências Exatas, Universidade Federal de Minas Gerais;Instituto de Ciências Exatas e Biológicas, Universidade Federal de Ouro Preto
关键词: Trust;    Type systems;    Proof assistants;    Soundness proofs;   
DOI  :  10.1007/s13173-013-0119-5
来源: Springer U K
PDF
【 摘 要 】

As computer programs become increasingly complex, techniques for ensuring trustworthiness of information manipulated by them become critical. In this work, we use the Coq proof assistant to formalise a $$\lambda $$ -calculus with trust types, originally formulated by Ørbæk and Palsberg. We give formal proofs of type soundness, erasure and simulation theorems and also prove decidability of the typing problem. As a result of our formalisation a certified type checker is derived.

【 授权许可】

Unknown   

【 预 览 】
附件列表
Files Size Format View
RO202106300003068ZK.pdf 1712KB PDF download
  文献评价指标  
  下载次数:11次 浏览次数:2次