×

Trust in the \(\lambda\)-calculus. (English) Zbl 0918.03013

Summary: 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 is presented as annotations of the underlying Curry types, and type inference is computable in \(O(n^3)\) time.

MSC:

03B40 Combinatory logic and lambda calculus
03B70 Logic in computer science
68N01 General topics in the theory of software
PDFBibTeX XMLCite
Full Text: DOI