Article

Free access

A core calculus of dependency

Authors:

Anindya Banerjee,

Jon G. RieckeAuthors Info & Claims

POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 147 - 160

https://doi.org/10.1145/292540.292555

Published: 01 January 1999 Publication History

Abstract

Notions of program dependency arise in many settings: security, partial evaluation, program slicing, and call-tracking. We argue that there is a central notion of dependency common to these settings that can be captured within a single calculus, the Dependency Core Calculus (DCC), a small extension of Moggi's computational lambda calculus. To establish this thesis, we translate typed calculi for secure information flow, binding-time analysis, slicing, and call-tracking into DCC. The translations help clarify aspects of the source calculi. We also define a semantic model for DCC and use it to give simple proofs of noninterference results for each case.

References

[1]

M. Abadi. Secrecy by typing in security protocols. In Theoretical Aspects of Computer Software: Third international Symposium, volume 1281 of Lect. Notes in Computer Sci. Springer-Verlag, 1997.

Digital Library

[2]

M. Abadi, B. Lampson, and J.-J. L6vy. Analysis and caching of dependencies. In Proceedings .of the 1996 ACM SIGPLAN International Conference on Functional Programming, pages 83-91. ACM, 1996.

Digital Library

[3]

S. K. Biswas. Dynamic Slicing in Higher-Order Programming Languages. PhD thesis, University of Pennsylvania, 1997.

Digital Library

[4]

R. Cartwright and M. Felleisen. The semantics of program dependence. In Proceedings of the 1989 ACM SIGPLAN Conference on Programming Language Design and implementation, pages 13-27. ACM, 1989.

Digital Library

[5]

C. Consel. Binding time analysis for higher order untyped functional languages. In Proceedings of the 1990 A CM Conference on Lisp and Functional Programming, pages 264- 272. ACM, 1990.

Digital Library

[6]

R. Davies. A temporal-logic approach to binding-time analysis. in Proceedings, Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 184-195, 1996.

Digital Library

[7]

R. Davies and F. Pfenning. A modal analysis of staged computation. In Conference Record of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, pages 258-270. ACM, 1996.

Digital Library

[8]

D. Denning. A lattice model of secure information flow. Commun. ACM, 19(5):236-242, 1976.

Digital Library

[9]

D. Denning and P. Denning. Certification of programs for secure information flow. Commun. ACM, 20(7):504-513, 1977.

Digital Library

[10]

M. Felleisen. The theory and practice of first-class prompts. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 180- 190. ACM, 1988.

Digital Library

[11]

J. Ferrante, K. J. Ottenstein, and J. D. Warren. The program dependence graph and its use in optimization. ACM Trans. Programming Languages and Systems, 9(3):319-349, 1987.

Digital Library

[12]

J. Hatcliff and O. Danvy. A computational formalization for partial evaluation. Mathematical Structures in Computer Science, 7:507-541, 1997. Special issue containing selected papers presented at the 1995 Workshop on Logic, Domains, and Programming Languages, Darmstadt, Germany.

Digital Library

[13]

N. Heintze and J. G. Riecke. The SLam calculus: programming with secrecy and integrity. In Conference Record of the Twenty-Fifth Annual ACM Symposium on Principles of Programming Languages, pages 365-377. ACM, 1998.

Digital Library

[14]

B. T. Howard. Inductive, coinductive, and pointed types. In Proceedings of the 1996 A CM SIGPLAN International Conference on Functional Programming, pages 102-109. ACM, 1996.

Digital Library

[15]

P. Hudak, S. L. Peyton Jones, P. L. Wadler, Arvind, B. Boutel, J. Fairbairn, J. Fasel, M. Guzman, K. Hammond, J. Hughes, T. Johnsson, R. Kieburtz, R. S. Nikhil, W. Partain, and J. Peterson. Report on the functional programming language Haskell, Version 1.2. ACM SIGPLAN Notices, May 1992.

[16]

J. Lambek and P. Scott. Introduction to higher order categorical logic. Cambridge studies in advanced mathematics. Cambridge University Press, 1986.

Digital Library

[17]

J. McLean. Security models. In J. Marciniak, editor, Encyclopedia of Software Engineering. Wiley Press, 1994.

[18]

J. C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.

Digital Library

[19]

M. Mizuno and D. A. Schmidt. A security flow control algorithm and its denotational semantics correctness proof. Formal Aspects of Computing, 4:727-754, 1992.

[20]

E. Moggi. Notions of computation and monads. Information and Control, 93:55-92, 199I.

Digital Library

[21]

E. Moggi. A categorical account of two-level languages. In Proceedings, Mathematical Foundations of Programming Semantics, Thirteenth Annual Conference, Electronic Notes in Theoretical Computer Science. Elsevier, 1997. Available from http : //www. elsevier, nl / locate/entcs/.

[22]

A. C. Myers and B. Liskov. A decentralized model for information flow control. In Proceedings of the Sixteenth A CM Symposium on Operating Systems Principles. ACM Press, 1997.

Digital Library

[23]

A. C. Myers. Practical mostly-static information flow control. In Conference Record of the Twenty-sixth Annual ACM Symposium on Principles of Programming Languages. ACM, 1999.

Digital Library

[24]

E Nielson. Strictness analysis and denotational abstract interpretation. In Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, pages 120-131. ACM, 1987.

Digital Library

[25]

H. R. Nielson and F. Nielson. Automatic binding time analysis for a typed ~ calculus. Science of Computer Programming, 10:139-176, 1988.

Digital Library

[26]

H. R. Nielson and E Nielson. Two-Level Functional Languages, volume 34 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

Digital Library

[27]

P. ~rb~ek and J. Palsberg. Trust in the L-calculus. Journal of Functional Programming, 7(6):557-591, November 1997.

Digital Library

[28]

J. C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513-523. North Holland, Amsterdam, 1983.

[29]

J. G. Riecke and R. Viswanathan. Isolating side effects in sequential languages. In Conference Record of the Twenty- Second Annual A CM Symposium on Principles of Programming Languages, pages 1-12. ACM, 1995.

Digital Library

[30]

A. Sabelfeld and David Sands. A Per model of secure information flow in sequential programs. Unpublished manuscript, 1998.

[31]

G. Smith and D. Volpano. Secure information flow in a multithreaded imperative language. In Conference Record of the Twenty-Fifth Annual A CM Symposium on Principles of Programming Languages. ACM, 1998.

Digital Library

[32]

C. Strachey. The varieties of programming language. In Proceedings of the International Computing Symposium, pages 222-233. Cini Foundation, Venice, 1972. Reprinted in Peter O'Hearn and Robert Tennent, eds., Algol-like Languages. Birkh~iuser, 1997.

[33]

~.-M. Tang. Systbmes d'effet et interprgtation abstraite pour l'analyse de riot de contrOle. PhD thesis, Ecole Nationale Suprriere des Mines de Paris, 1994.

[34]

Y.-M. Tang and P. Jouvelot. Effect systems with subtyping. In ACM Conference on Partial Evaluation and Program Manipulation, June 1995.

Digital Library

[35]

P. Thiemann. A unified framework for binding-time analysis. In M. Bidoit, editor, Colloquium on Formal Approaches in Software Engineering (FASE '97), volume 1214 of Lect. Notes in Computer Sci., pages 742-756. Springer-Verlag, April 1997.

Digital Library

[36]

F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3(3): 121-189, September 1995.

[37]

M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2): 109-176, 1997.

Digital Library

[38]

D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(3): 1- 21, 1996.

Digital Library

[39]

P. Wadler. The marriage of effects and monads. In Proceedings of the 1998 A CM SIGPLAN International Conference on Functional Programming, pages 63-74. ACM, 1998.

Digital Library

[40]

M. Weiser. Program slicing. IEEE Trans. Software Engineering, 10(4):352-357, July 1984.

Digital Library

Cited By

Li JWang EZhang Y(2024)Compiling Probabilistic Programs for Variable Elimination with Information FlowProceedings of the ACM on Programming Languages10.1145/36564488:PLDI(1755-1780)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656448
Lamba ATaylor MBeardsley VBambeck JBond MLin Z(2024)Cocoon: Static Information Flow Control in RustProceedings of the ACM on Programming Languages10.1145/36498178:OOPSLA1(166-193)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649817
Liu YChan JShi JWeirich S(2024)Internalizing Indistinguishability with Dependent TypesProceedings of the ACM on Programming Languages10.1145/36328868:POPL(1298-1325)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632886
Show More Cited By

Index Terms

A core calculus of dependency

Recommendations

A Perspective on the Dependency Core Calculus
PLAS '18: Proceedings of the 13th Workshop on Programming Languages and Analysis for Security

This paper presents a simple but equally expressive vari- ant on the terminating fragment of the Dependency Core Calculus (DCC) of Abadi et al. [2]. DCC is a concise and elegant calculus for tracking dependency. The calculus has applications in, among ...
Access control in a core calculus of dependency
ICFP '06: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming

The Dependency Core Calculus (DCC) is an extension of the computational lambda calculus that was designed in order to capture the notion of dependency that arises in information-flow control, partial evaluation, and other programming-language settings. ...
The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value
PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming

We introduce and study the Bang Calculus, an untyped functional calculus in which the promotion operation of Linear Logic is made explicit and where application is a bilinear operation. This calculus, which can be understood as an untyped version of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 1999

324 pages

ISBN:1581130953

DOI:10.1145/292540

Chairmen:
Andrew Appel
Princeton Univ., Princeton, NJ
,
Alex Aiken
Univ. of California, Berkeley

Copyright © 1999 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1999

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL99

Sponsor:

POPL99: Symposium on Prinicples of Programming Languages 1999

January 20 - 22, 1999

Texas, San Antonio, USA

Acceptance Rates

POPL '99 Paper Acceptance Rate 24 of 136 submissions, 18%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

373
Total Citations
View Citations
1,723
Total Downloads

Downloads (Last 12 months)283
Downloads (Last 6 weeks)26

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Li JWang EZhang Y(2024)Compiling Probabilistic Programs for Variable Elimination with Information FlowProceedings of the ACM on Programming Languages10.1145/36564488:PLDI(1755-1780)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656448
Lamba ATaylor MBeardsley VBambeck JBond MLin Z(2024)Cocoon: Static Information Flow Control in RustProceedings of the ACM on Programming Languages10.1145/36498178:OOPSLA1(166-193)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649817
Liu YChan JShi JWeirich S(2024)Internalizing Indistinguishability with Dependent TypesProceedings of the ACM on Programming Languages10.1145/36328868:POPL(1298-1325)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632886
Geraldo ECosta Seco JHildebrandt T(2023)Data-Dependent Confidentiality in DCR GraphsProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610619(1-13)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1145/3610612.3610619
Choudhury P(2022)Monadic and comonadic aspects of dependency analysisProceedings of the ACM on Programming Languages10.1145/35633356:OOPSLA2(1320-1348)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563335
Yoon IZakowski YZdancewic S(2022)Formal reasoning about layered monadic interpretersProceedings of the ACM on Programming Languages10.1145/35476306:ICFP(254-282)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547630
Crichton WPatrignani MAgrawala MHanrahan PJhala RDillig I(2022)Modular information flow through ownershipProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523445(1-14)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523445
Dal Lago UGavazzo F(2022)A relational theory of effects and coeffectsProceedings of the ACM on Programming Languages10.1145/34986926:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498692
Choudhury PEades HWeirich S(2022)A Dependent Dependency CalculusProgramming Languages and Systems10.1007/978-3-030-99336-8_15(403-430)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99336-8_15
Wood JAtkey R(2022)A Framework for Substructural Type SystemsProgramming Languages and Systems10.1007/978-3-030-99336-8_14(376-402)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99336-8_14
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents