Open AccessTrust in the lambda-calculus
Author(s) -
Jens Palsberg,
Peter Ørbæk
Publication year - 1995
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v2i31.19934
Subject(s) - programmer , computer science , type (biology) , programming language , function (biology) , calculus (dental) , property (philosophy) , inference , discrete mathematics , mathematics , theoretical computer science , artificial intelligence , philosophy , epistemology , medicine , ecology , dentistry , evolutionary biology , biology
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.