Trust in the lambda-calculus

Abstract

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