Trust in the Lambda-Calculus

Mar 28, 1997

Abstract

We introduce 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 is presented as annotations of the underlying Curry types, and type inference is computable in O(n3) time. Our calculus can be seen as a minimal API for trust-programming.

This is joint work with Peter Orbaek.