Abstract
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 trusttype 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(n3) time.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J.-P. Banâtre, C. Bryce, and D. L. Metayer. Compile-time detection of information flow in sequential programs. In D. Gollmann, editor, Computer Security — ESORICS 94, 3rd European Symp. on Research in Comp. Security, pages 55–73. Springer-Verlag (LNCS 875), 1994.
H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, 1981.
G. L. Burn, C. Hankin, and S. Abramsky. Strictness analysis for higher-order functions. Sci. Comput. Programming, 7:249–278, 1986.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Fourth ACM Symposium on Principles of Programming Languages, pages 238–252, 1977.
D. E. Denning and P. J. Denning. Certifications of programs for secure information flow. Commun. ACM, 20(7):504–512, July 1977.
T. Freeman and F. Pfenning. Refinement types for ML. In Proc. ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation, 1991.
C. K. Gomard and N. D. Jones. A partial evaluator for the untyped lambdacalculus. Journal of Functional Programming, 1(1):21–69, 1991.
F. Henglein. Dynamic typing. In Proc. ESOP'92, European Symposium on Programming, pages 233–253. Springer-Verlag (LNCS 582), 1992.
F. Henglein and J. Jørgensen. Formally optimal boxing. In Proc. POPL'94, 21st Annual Symposium on Principles of Programming Languages, pages 213–226, 1994.
D. Kozen, J. Palsberg, and M. I. Schwartzbach. Efficient inference of partial types. J. Comput. Syst. Sci., 49(2):306–324, 1994. Also in Proc. FOCS'92, 33rd IEEE Symposium on Foundations of Computer Science, pages 363–371, Pittsburgh, Pennsylvania, October 1992.
T.-M. Kuo and P. Mishra. Strictness analysis: A new perspective based on type inference. In Proc. Conference on Functional Programming Languages and Computer Architecture, pages 260–272, 1989.
J. Mitchell. Coercion and type inference. In Eleventh Symposium on Principles of Programming Languages, pages 175–185, 1984.
M. Mizuno and D. Schmidt. A security flow control algorithm and its denotational semantics correctness proof. Technical Report TR-CS-90-21, Kansas State University, 1990.
P. Ørbæk. Can you trust your data? In P. D. Mosses, editor, Proc. TAPSOFT'95, Theory and Practice of Software Development, pages 575–590. Springer-Verlag (LNCS 915), 1995.
J. Palsberg. Efficient inference of object types. Information and Computation. To appear. Also in Proc. LICS'94, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 186–195, Paris, France, July 1994.
J. Palsberg and P. Ørbaek. Trust in the λ-calculus. Technical Report BRICS RS-95-31, BRICS, Computer Science Department, Aarhus University, 1995. URL: http://www.daimi.aau.dk/BRICS.
J. Palsberg and M. I. Schwartzbach. Safety analysis versus type inference for partial types. Inf. Process. Lett., 43:175–180, 1992.
J. Palsberg and M. I. Schwartzbach. Safety analysis versus type inference. Information and Computation, 118(1):128–141, 1995.
J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):245–271, 1992.
M. Wand. Type inference for record concatenation and multiple inheritance. Information and Computation, 93(1):1–15, 1991.
D. A. Wright. A new technique for strictness analysis. In Proc. TAPSOFT'91, pages 235–258. Springer-Verlag (LNCS 494), 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Palsberg, J., Ørb⇓ek, P. (1995). Trust in the λ-calculus. In: Mycroft, A. (eds) Static Analysis. SAS 1995. Lecture Notes in Computer Science, vol 983. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60360-3_47
Download citation
DOI: https://doi.org/10.1007/3-540-60360-3_47
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60360-3
Online ISBN: 978-3-540-45050-4
eBook Packages: Springer Book Archive