Mar 28, 1997
"Trust in the Lambda-Calculus"
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.
Unless otherwise noted, the security seminar is held on Wednesdays at 4:30P.M.
STEW G52 (Suite 050B), West Lafayette Campus. More information...