Mechanized metatheory for a $$lambda $$ λ -calculus with trust types

摘要

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.