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.

Full Abstraction for Nominal Scott Domains

(Link).

Authors: Steffen Lösch and Andrew M. Pitts (University of Cambridge).

Conference / Reference: 40th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL '13), 23-25 January 2013, Rome, Italy (ACM Press).

Comments: Just two weeks ago I was remarking on the very large proportion of papers recommended by Google Scholar Updates that came from Cambridge; well, here is another one - the fourth of the last six. To be precise, I should say it was the fourth of the last eight, as I have decided to fudge the purity of the experiment for the first time by skipping two papers from the same authors as this this one, on the grounds that I was unlikely to gain much benefit from them.

This paper, whose second author was my PhD supervisor, is much more down my alley, as you might expect; it is another that deals with nominal sets, which I first discussed on this blog here. In that post I mentioned in passing that nominal sets had their origins in 1930s axiomatic set theory, before a rather surprising revival in 1999 by Murdoch Gabbay and Andrew Pitts, who employed them to model syntax with names and binders in computing. However their origins in deep set theory shouldn't be completely forgotten; their original use was for an attempt to construct a model of set theory where the axiom of choice failed.

Mathematics as conceived by Euclid is the process of enumerating axioms and inference rules that are obviously true, and then deriving truths from them (some of which may be far from obvious). Even in Euclid's own work this idealised picture did not really hold, as the fifth postulate of his geometry, regarding non-parallel lines, was rather more complicated that might be desired, and was long regarded as a flaw of his presentation. Much later it turned out that denying this postulate could lead to interesting and valuable mathematics for geometry in curved space. The attempt to axiomatise set theory in the early twentieth century came to a quite similar place, with the axiom of choice (which regards the ability to make systematic choices from unstructured sets, even infinite ones) as the useful but non-obvious 'rogue' axiom. Again, it turned out that both the axiom and its negation were compatible with the other, more obvious, set axioms, and so 'nonstandard set theory' in which the axiom failed - of which nominal sets are an example - could be developed and applied, as with non-Euclidean geometry.

The subjects of this paper, domain theory and denotational semantics, are techniques to interpret computer programs as objects in a mathematical setting that directly supports rich and complex computation phenomena such as recursion. This apparently esoteric material about set theoretic axioms matters because some of the proofs of the basic facts about domains use the axiom of choice. This paper defines a programming language PNA (and an extension, PNA+) with commands for manipulating and binding names, and develops domain theory within nominal sets to provide a characterisation of programs in this language. But domain theory within nominal sets needs, in part, to be reconstructed to avoid reliance on the now invalid axiom, which is one of interesting technical challenges addressed by this work (following earlier work by Glynn Winskel and David Turner (pdf), also at Cambridge).