期刊论文详细信息
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 | |
![]() |
【 摘 要 】
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 | ![]() |