Discussing "A Core Calculus of Dependency"

(Link)

Authors: Martín Abadi (Compaq Systems Research Center) and Anindya Banerjee (Stevens Institute of Technology) and Nevin Heintze (Bell Laboratories) and Jon G. Riecke (Bell Laboratories)

Reference: Abadi, Martín, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. "A core calculus of dependency." In POPL ’99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 147-160. 1999.

Why this paper? Cited by The Syntactic Dual of Autonomous Categories Enriched over Generalised Metric Spaces and Recursive Session Logical Relations.

This paper concerns the general concept of programming languages and formal calculi whose types record how certain parts of a program might depend on others. One example is the SLam (Secure Lambda) Calculus of Heintze and Riecke, where types are annotated by the level of security of the data held in them. These annotations are used to prevent the output of low security computations from depending on more private information, as that creates the risk of secrets being leaked. Another example is the slicing calculus of Abadi and coauthors, where types record which parts of the program the output might depend on, which was designed to be applied to caching rather than security. This paper unifies these concepts, and more, into the Dependency Core Calculus (DCC).

The technology they adapt for this purpose comes from a paper I looked at on this blog only a month ago, Moggi’s monadic metalanguage! There, type constructors called monads captured various notions of side effect. Here, a monad is introduced for each element of a hierarchy; for example, if there are a certain number of security levels, then there will be a monad for each such level. By reducing various calculi to DCC they can prove desirable properties for each them, and even comment on alternative design decisions that could be made for them. Semantics for DCC are given in terms of sets equipped with certain relations called complete partial orders, arranged into a category.

One somewhat interesting note is that three of the four authors were employed by the research labs of private corporations, rather than research universities. Private researchers making their work available to the scientific commons via publication is not as rare as some might expect, but there is some evidence that this practice is declining.