Discussing "First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees"

(Link). Slightly confusingly, the authors earlier published a shorter conference article with the same name.

Authors: Lars Birkedal (IT University of Copenhagen), Rasmus Ejlers Møgelberg (IT University of Copenhagen), Jan Schwinghammer (Saarland University), and Kristian Støvring (University of Copenhagen)

Reference: Birkedal, L., Møgelberg, R. E., Schwinghammer, J., & Støvring, K. (2012). First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science, 8.

Why this paper? Cited by A Formal Logic for Formal Category Theory, Classifying topoi in synthetic guarded domain theory, and A metalanguage for cost-aware denotational semantics

This paper, which has been very influential on a chunk of my career, nicely pieces together some practically minded applications in program verification with the more abstract world of category theory.

The practical motivations are very similar to the step-indexing paper I discussed a few weeks ago, namely type systems with recursive features that appear difficult to reason about without getting trapped in unsolvable circularities. In the key example of this paper, a programming language with higher-order store (i.e. the ability to store typed programs in memory) forces one to define the meaning of types in terms of the meaning of the store, but also to define the meaning of the store in terms of the meanings of types! In the step-indexing approach, one works around these circularities by invoking a natural number that decreases towards zero as the program computes; this paper does something quite similar, but in the name of “avoiding tedious calculations with step indices” it instead asks us to work in a topos which naturally supports this sort of notion of steps.

A topos is, very roughly, a ‘mathematical universe’ (or category) which contains the mathematical machinery one would expect to have in set theory. For example, a subobject classifier is an object of truth values. We might expect to have just the two values, True and False – and indeed there are toposes for which this is so – but in the topos of this paper, the topos of trees, one can see the subobject classifier as the set of all natural numbers, along with the infinite value ω. One can consider 0 as False, ω as True, and each positive integer n as ‘not falsified by the first n steps of computation’ (this is not quite how this paper presents things, but is the point of view taken for example by a later paper of mine). This is quite a nice way to think about computations that unfold over time: consider two streams (infinite lists); they are 1-equal if their first elements agree, 2-equal if their first two elements agree, and so on to only reach ω, or ‘true’, equality if there is no index on which they will ever be unequal. In other words, working inside the topos of trees gives you access to a logic that allows you to talk about certain aspects of computer programs that are harder to describe with more conventional logic. In particular, instead of working directly with the indices, one instead can do a lot with a modality (new logical connective) called ‘later’ than helps hide those details away while preserving the ability to make the sort of arguments for which one would otherwise explicitly involve step indices.

As well as the logical point of view which comes from working with the subobject classifier, one can also use the topos of trees as a denotational semantics (mathematical meaning) for types in various ways, whether one is reasoning about a typed programming language, or using dependent type theory to construct a formal mathematical argument. Looked at through this prism, instead of viewing a type as standing in for its set of elements, one can view types as an infinite series of sets that become more and more precise or informative over time. For example, the type of streams is not merely the set of infinite sequences, but instead an infinite string of sets that at step 1 reveal only their first elements, at step 2 reveal their first two elements, and so on. The modality `later’ now reappears in slightly different guise as a type-former; one needs to check that self-references are guarded by later in order to ensure one has a meaningful recursive type definition. This idea of checking syntax for guardedness in order to ensure that recursive definitions are good is quite old, but usually takes place at the level of the syntax of terms. By lifting this check to the level of types we get the advantages that well-behaved type systems usually confer, particularly modularity – the ability to stick any two good programs together, provided their types agree, without their combination going wrong.

Discussing "The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logics"

 (Link)

Author: Arnon Avron (Tel Aviv University)

Reference: Arnon Avron. The method of hypersequents in the proof theory of propositional non-classical logics. In Wilfrid Hodges, Martin Hyland, Charles Steinhorn, and John Truss, editors, Logic: From Foundations to Applications: European Logic Colloquium, page 1–32. Clarendon Press, USA, 1996.

Why this paper? Cited by Nested Sequents for First-Order Modal Logics via Reachability Rules and Falsification-Aware Calculi and Semantics for Normal Modal Logics Including S4 and S5

This paper returns us to the world of structural proof theory, and in particular the sequent calculus, a formalism for organising and (often) generating proofs in various logics. The `various logics’ part of that phrase is very important here – there are a huge number of different logics out there, capturing different notions of truth and ways of combining propositions. Unfortunately many of these logics do not, in any obvious way, lend themselves to a well behaved sequent calculus. This paper reviews some work on a more flexible generalisation of sequent calculus based on hypersequents.

A sequent is simply a list of assumptions (or premises) and a list of conclusions. Working with a list of all current assumptions is very natural, but a list of conclusions may seem more unusual. The intuition is to view that list as disjunctive, i.e. proving any one of the conclusions will do. Working with a list of conclusions rather than a single one is not necessary for every logic, but turns out to be important for some. Similarly, hypersequents are simply a list of sequents, typically viewed as a disjunction. As for standard sequents, this is pointless for some logics but does allow other logics to be handled that would otherwise resist a nice structural treatment. The magic of this is that we can create new proof rules that allow sequents to communicate with each other within the hypersequent, for example by exchanging conclusions between them, in ways that allow the proof of new theorems.

Hypersequent calculi are shown to exist for a variety of interesting logics. We see Gödel–Dummett logic, also known as Dummett’s LC, a logic in which propositions can be assigned a position on an infinitely long truth spectrum, with one proposition implying another if the second proposition is ‘more true’ than the first; the relevance logic RM, which can be understood via the Sugihara matrix - truth values range across the integers, with the non-negative integers designated as ‘true’, and logical negation exactly matching the negation of integers; S5, a long established member of the family of modal logics that resisted the toolkit of standard proof theory; and a couple of three-valued logics which allow for a single intermediate position between absolute truth and falsity.

Discussing "Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type"

(Link)

Authors: Thorsten Altenkirch (University of Nottingham), Nils Anders Danielsson (University of Gothenburg), Nicolai Kraus (University of Nottingham)

Reference: Altenkirch, T., Danielsson, N.A., Kraus, N. (2017). Partiality, Revisited. In: Esparza, J., Murawski, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2017. Lecture Notes in Computer Science(), vol 10203. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-54458-7_31

Why this paper? Cited by A metalanguage for cost-aware denotational semantics, and Streams of Approximations, Equivalence of Recursive Effectful Programs, and Executable Denotational Semantics with Interaction Trees

A couple of months ago I wrote about Moggi’s seminal work on monads, which can be used both to write, and to reason about, code with side effects. A side effect is any operation of a program which is not most naturally thought of as an output, and this paper concentrates on one such notion – the program potentially failing to terminate and produce an output at all. The option to fail to terminate is a crucial feature of most real programming languages, because without it, a language fails Turing completeness, and so is not as expressive as it might be.

Following Capretta, possible non-termination can be modelled by the delay monad. This is a construction which allows outputs to be ‘delayed’ any number of times, and perhaps indefinitely. Elements of the monad therefore carry a trace of how many times they were delayed - very roughly speaking, how many steps of some computation was required to produce them, a concept we have seen before. However for some purposes in reasoning about programs, one wishes to ignore the number of steps taken, and merely talk about the output (if there was one). We do this by quotienting the monad to ignore any finite number of delays. This makes the delay monad a monad in the category of setoids – sets equipped with an equivalence relation.

Unfortunately working formally with setoids may consign one to what is colourfully called ‘setoid hell’, where one has the tedium of proving that every construction, no matter how apparently unconnected to the notions of termination and delay, must respect the equivalence relation. An alternative is working in a type theory with quotient types, but this turns out not to work as well as expected, either failing to produce a monad (and hence, a well behaved model of the side effect) at all, or requiring a powerful extra mathematical property called countable choice to make things work.

This paper is influential because it shows that a proper delay monad can be constructed without invoking any new mathematical axioms if we allow ourselves to construct quotient inductive-inductive types (QIITs). Quotient inductive types are a limited form of the higher inductive types of homotopy type theory; the ‘inductive-inductive’ part of the term means that a type and a construction on the type are defined inductively at the same time. Given this technology, the delay monad, quotiented by ignoring finite numbers of delays, is finally shown to behave as it should.

Discussing "Iris from the ground up: A modular foundation for higher-order concurrent separation logic"

(Link)

Authors: Ralf Jung (Max Planck Institute for Software Systems), Robbert Krebbers (Delft University of Technology), Jacques-Henri Jourdan (Max Planck Institute for Software Systems), Aleš Bizjak (Aarhus University), Lars Birkedal (Aarhus University), Derek Dreyer (Max Planck Institute for Software Systems)

Reference: JUNG, R., KREBBERS, R., JOURDAN, J., BIZJAK, A., BIRKEDAL, L., & DREYER, D. (2018). Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28, E20. doi:10.1017/S0956796818000151

Why this paper? Cited by A Decision Procedure for Guarded Separation Logic, Mechanised Robust Safety for Virtual Machines Communicating above FF-A, and Fractional Resources in Unbounded Separation Logic

This 2018 paper is more recent than most I get referred to by the citations in my Google Scholar recommendations, but there’s no doubting the relevance to me given that three of the authors (Robbert, Aleš, and Lars) are former colleagues at Aarhus University’s Logic and Semantics Group.

This paper summarises a series of papers from 2014 on, developing a logic called Iris. This is the latest evolution of separation logic (and, in turn, Hoare logic) for reasoning formally about the correctness of programs. The game here has been to add more advanced functionality to allow reasoning about programs written in a variety of programming languages without blowing up the logic to unreasonable size and complexity. As such, Iris is packed with features which encompass some I’ve written about already in the blog, such as permissions and step-indexing, along with many others such as various notions of concurrency and higher-order store. Many of these features are derivable via a small(ish) core logic, and the whole framework is usable in the interactive theorem prover Coq to facilitate fully formal, machine-checked proofs.

I will not be attempting to exhaustively summarise a 73 page paper in a short blog post, but to take one example of the flexibility of the logic, an Iris user can define their own ‘camera’ which defines the notion of state they want to invoke separation with respect to, whether it be Reynolds’s old notion of the physical memory, or some more exotic notion of `ghost state’ which does not directly relate to physical state.

Discussing "Checking Interference with Fractional Permissions"

(Link)

Author: John Boyland (University of Wisconsin-Milwaukee)

Reference: Boyland, J. (2003). Checking Interference with Fractional Permissions. In: Cousot, R. (eds) Static Analysis. SAS 2003. Lecture Notes in Computer Science, vol 2694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44898-5_4

Why this paper? Cited by Mechanised Robust Safety for Virtual Machines Communicating above FF-A, and Fractional Resources in Unbounded Separation Logic, and Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version)

Of late the citations in my Google Scholar recommendations have been very concerned with the question of whether two different parts of a program interfere with each other, or depend on each other – see here, here, and (less directly) here. This is an important question if we want to reason about the behaviour of a program – we would like to reason about a large program piece by piece, but can only do so if we are sure the pieces do not interfere with each other (or, if they do interfere, we have a precise sense of how this interference might manifest).

Separation logic à la Reynolds tells us that we can reason about parts of a program separately if they only access disjoint parts of memory. This is correct, but needlessly blunt. Two programs that read the same piece of memory do not effect each other; it is only if one of those program write to memory the other program is interested in that we have an issue. The solution proposed in this paper is to give different (parts of) programs different levels of permission to each part of the memory. Full permission, represented by the number 1, allows one to write and read, whereas a permission represented by a fraction strictly between 0 and 1 gives only read access. Where there is parallel composition or similar in the program, permissions can be divided between threads. Conversely, a program can add its permissions back together when it completes threads and hence, if full permission is reached, regain the ability to write.

The concepts of this paper and presented in the form of a type system, but it was soon realised by others that they can also be used to generalise separation logic as well; this is the context in which fractional permissions continue to appear in papers recommended to me.

Discussing "Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types"

 (Link)

Author: Amal Ahmed (Harvard University)

Reference: Ahmed, A. (2006). Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In: Sestoft, P. (eds) Programming Languages and Systems. ESOP 2006. Lecture Notes in Computer Science, vol 3924. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11693024_6

Why this paper? Cited by Fractional Resources in Unbounded Separation Logic, and Program Equivalence in an Untyped, Call-by-value Lambda Calculus with Uncurried Recursive Functions, and Recursive Session Logical Relations

When are two programs equivalent? There are various answers one can give to this depending on whether one wishes to consider factors like time and memory usage, but one fundamental notion is contextual equivalence: two programs A and B are equivalent in this sense if any program in the language with A as a component will behave the same (with respect to termination) if that component is replaced by B. Hence, there is no context which can tell them apart. This is an intrinsically difficult fact to prove because one must consider all possible contexts, of which there are infinitely many to choose from. A general technique for demonstrating contextual equivalence in typed languages is the method of logical relations, in which a general relation between programs is built up by induction on types, and the problem of proving equivalence for particular programs is narrowed to the problem of proving that these programs are related.

The problem with defining a relation in the inductive style is that it relies on types being defined in terms of simpler subtypes. This paper looks at two important type constructors for which this fails. Inductive types like lists and trees refer to themselves – lists are defined in terms of lists – in a way that would make a naïve inductive definition on them immediately circular. Quantified types – universal types for parametric polymorphism and existential types, which resemble abstract data types – contain type variables which can be replaced by arbitrarily complicated types. This paper, picking up an idea from Appel and McAllester, shows that the unpleasant circularities can be removed if one adds a natural number ‘step-index’ to the relation to make sure that the induction remains well defined – when one is working with a type and must consider a type that is not smaller, one reduces the step-index towards zero to compensate. A lot is proved about this style of reasoning – the full version of the paper weighs in at a hefty 169 pages!

This is certainly a relevant ‘classic paper’ with respect to my own research interests; I get involved in this area via later work by Birkedal, Møgelberg, Schwinghammer and Støvring on ‘synthetic’ step-indexing, which uses a modality to hide some of the arithmetic of step-indexing. But that is, perhaps, a topic for another day.

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.