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.