Ribeiro, Rodrigo GeraldoFigueiredo, Lucília Camarão deFigueiredo, Carlos Camarão de2017-02-012017-02-012013RIBEIRO, R. G.; FIGUEIREDO, L. C. de; FIGUEIREDO, C. C. de. Mechanized metatheory for a λ-calculus with trust types. Journal of the Brazilian Computer Society, v. 19, n. 4, p. 433-443, nov. 2013. Disponível em: <https://link.springer.com/article/10.1007/s13173-013-0119-5>. Acesso em: 23 jan. 2017.1678-4804http://www.repositorio.ufop.br/handle/123456789/7173As 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 λ-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.en-USabertoType systemsProof assistantsSoundness proofsArtigo publicado em periodicohttps://link.springer.com/article/10.1007/s13173-013-0119-5https://doi.org/10.1007/s13173-013-0119-5