Hostname: page-component-745bb68f8f-s22k5 Total loading time: 0 Render date: 2025-01-12T05:34:29.399Z Has data issue: false hasContentIssue false
  • English
  • Français

Trust in the λ-calculus

Published online by Cambridge University Press:  01 November 1997

P. ØRBÆK  and
J. PALSBERG
P. ØRBÆK
Affiliation:
BRICS, Centre of the Danish National Research Foundation, Dept. of Computer Science, University of Aarhus, Ny Munkegade bld 540, 8000 Aarhus C, Denmark
J. PALSBERG
Affiliation:
BRICS, Centre of the Danish National Research Foundation, Dept. of Computer Science, University of Aarhus, Ny Munkegade bld 540, 8000 Aarhus C, Denmark
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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 λ-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.

Type
Research Article
Information
Journal of Functional Programming , Volume 7 , Issue 6 , November 1997 , pp. 557 - 591
Copyright
© 1997 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.