Abstract
Dependency has been identified as the main ingredient underlying many program analyses, in particular flow analysis, secrecy and integrity analysis, and binding-time analysis. Driven by that insight, Abadi, Banerjee, Heintze, and Riecke [1] have defined a dependency core calculus (DCC). DCC serves as a common target language for defining the above analyses by translation to DCC.
The present work considers the opposite direction. We define a Prototype Dependency Calculus (PDC) and define flow analysis, secrecy analysis, and region analysis by translation from PDC.
Chapter PDF
Similar content being viewed by others
References
M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke. A core calculus of dependency. In A. Aiken, editor, Proc. 26th Annual ACM Symposium on Principles of Programming Languages, pages 147–160, San Antonio, Texas, USA, Jan. 1999. ACM Press.
M. Abadi, B. Lampson, and J.-J. Lévy. Analysis and caching of dependencies. In R. K. Dybvig, editor, Proc. International Conference on Functional Programming 1996, pages 83–91, Philadelphia, PA, May 1996. ACM Press, New York.
K. Asai. Binding-time analysis for both static and dynamic expressions. In Static Analysis, pages 117–133, 1999.
A. Banerjee, N. Heintze, and J. G. Riecke. Region analysis and the polymorphic lambda calculus. In Proc. of the 14th Annual IEEE Symposium on Logic in Computer Science, pages 88–97, Trento, Italy, July 1999. IEEE Computer Society Press.
L. Birkedal and M. Welinder. Binding-time analysis for Standard-ML. In P. Sestoft and H. Søndergaard, editors, Proc. ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation PEPM’ 94, pages 61–71, Orlando, Fla., June 1994. University of Melbourne, Australia. Technical Report 94/9, Department of Computer Science.
D. Dussart, F. Henglein, and C. Mossin. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In Mycroft [11], pages 118–136.
N. Heintze. Control-flow analysis and type systems. In Mycroft [11], pages 189–206.
N. Heintze and J. G. Riecke. The SLam calculus: Programming with security and integrity. In L. Cardelli, editor, Proc. 25th Annual ACM Symposium on Principles of Programming Languages, pages 365–377, San Diego, CA, USA, Jan. 1998. ACM Press.
F. Henglein and C. Mossin. Polymorphic binding-time analysis. In D. Sannella, editor, Proceedings of European Symposium on Programming, volume 788 of Lecture Notes in Computer Science, pages 287–301. Springer-Verlag, Apr. 1994.
E. Moggi. Notions of computations and monads. Information and Computation, 93:55–92, 1991.
A. Mycroft, editor. Proc. International Static Analysis Symposium, SAS’95, number 983 in Lecture Notes in Computer Science, Glasgow, Scotland, Sept. 1995. Springer-Verlag.
F. Nielson and H. R. Nielson. Automatic binding-time analysis for a typed lambda calculus. Science of Computer Programming, 10:139–176, 1988.
F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer Verlag, 1999.
H. R. Nielson, F. Nielson, and T. Amtoft. Polymorphic subtyping for effiect analysis: The static semantics. In M. Dam, editor, Proceedings of the Fifth LOMAPS Workshop, number 1192 in Lecture Notes in Computer Science. Springer-Verlag, 1997.
J. Palsberg and P. O’Keefe. A type system equivalent to flow analysis. In Proc. 22nd Annual ACM Symposium on Principles of Programming Languages, pages 367–378, San Francisco, CA, Jan. 1995. ACM Press. 239
P. Ørbæk and J. Palsberg. Trust in the λ-calculus. Journal of Functional Programming, 7(6):557–591, Nov. 1997.
J.-P. Talpin and P. Jouvelot. The type and effiect discipline. Information and Computation, 111(2):245–296, 1994.
Y. M. Tang and P. Jouvelot. Control-flow effiects for closure analysis. In Proceedings of the 2nd Workshop on Static Analysis, number 81-82 in Bigre Journal, pages 313–321, Bordeaux, France, Oct. 1992.
Y. M. Tang and P. Jouvelot. Effiect systems with subtyping. In W. Scherlis, editor, Proc. ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation PEPM’ 95, pages 45–53, La Jolla, CA, June 1995. ACM Press.
M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997.
D. Volpano and G. Smith. A type-based approach to program security. In M. Bidoit and M. Dauchet, editors, TAPSOFT’97: Theory and Practice of Software Development, number 1214 in Lecture Notes in Computer Science, pages 607–621, Lille, France, Apr. 1997. Springer-Verlag.
D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3):1–21, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thiemann, P. (2002). A Prototype Dependency Calculus. In: Le Métayer, D. (eds) Programming Languages and Systems. ESOP 2002. Lecture Notes in Computer Science, vol 2305. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45927-8_17
Download citation
DOI: https://doi.org/10.1007/3-540-45927-8_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43363-7
Online ISBN: 978-3-540-45927-9
eBook Packages: Springer Book Archive