Mechanized metatheory for a \(\lambda \) -calculus with trust types

Brazilian Computer Society. Journal

article

Rodrigo Ribeiro¹  Lucília Figueiredo²  Carlos Camarão¹ 

[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