Trust in the lambda-calculus

Abstract

This paper introduces trust analysis for higher-order languages. Trust<br />analysis encourages the programmer to make explicit the trustworthiness of<br />data, and in return it can guarantee that no mistakes with respect to trust will<br />be made at run-time. We present a confluent lambda-calculus with explicit trust<br />operations, and we equip it with a trust-type system which has the subject<br />reduction property. Trust information in presented as two annotations of each<br />function type constructor, and type inference is computable in O(n^3) time.