A Core Calculus of Dependency

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.

• Type: Conference
• Year: 1999
• Where: POPL
• Authors: Martín Abadi, Anindya Banerjee, Nevin Heintze, Jon G. Riecke
• Keywords: Computational Lambda Calculus, Dependency Core Calculus, POPL 1999, Program Dependency Arise, Programming Languages