Discussing "Internal Universes in Models of Homotopy Type Theory"

(Link)

Authors: Daniel R. Licata (Wesleyan University), Ian Orton (University of Cambridge), Andrew M. Pitts (University of Cambridge), and Bas Spitters (Aarhus University)

Reference: D. R. Licata, I. Orton, A. M. Pitts, and B. Spitters. “Internal Universes in Models of Homotopy Type Theory”. In: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Ed. by H. Kirchner. Vol. 108. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018, 22:1–22:17. doi: 10.4230/LIPIcs.FSCD.2018.22.

Why this paper? Cited by Homotopy type theory as internal languages of diagrams of ∞-logoses and mitten: a flexible multimodal proof assistant

Although this paper has among its authors my PhD supervisor (Andy) and a former collaborator (Bas), it did not give up its secrets easily, for me at least, thanks to the high technical level in the introduction alone. But, like an early Christmas present, I think there’ s something pretty interesting in here once it is unwrapped.

The story starts with homotopy type theory (on which I have written before), a proposal to improve the treatment of equality in the type-theoretic foundations of mathematics. It continues with cubical type theory, a first shot at actually implementing homotopy type theory. While homotopy type theory can be understood via a general notion of path-up-to-continuous-deformation in a space, cubical type theory is understood through a specific such space, namely the cubical sets. Never mind precisely what they are; it is enough for this less technical blog post to know that there is an interpretation of cubical type theory in some mathematical structure that allows one to give meaning to all constructions. One technicality that is important for understanding the paper of today is that the naïve approach to extracting a type theory from cubical sets (which can be done because the cubical sets form a topos) does not give quite the right thing. One needs the naïve notion of type to come equipped with something extra, called a composition structure; we call types with such structure fibrant. Not every cubical set is fibrant (else we would not have to explicitly require the structure). For example the interval cubical set which is used to define the notion of path, and hence equality, is not itself fibrant, so is not a first class type.

Today’s paper is part of an effort to define the correct notion of model of cubical type theory in type theory itself. This may seem quixotic but is in fact well motivated: such a definition is suitable for machine checking (and indeed this is done by formalising this paper in an Agda fork called Agda-flat), can be simpler than a more standard definition, and can also be more general, which raises the possibility of shifting from cubical sets to some other model if such a shift were found to be more appropriate for some purpose. However cubical sets are not abandoned altogether; the acid test for the type theory used in this paper is whether everything works in the ‘internal language’ of cubical sets (here again we use the fact that we have a topos, and any such comes equipped with its own native type theory).

The problem with the literature up until this paper is that attempts to formalise a model of cubical type theory in this style had not yet included any universe types. Universes are less cosmic than they sound (although the problems they throw up can be mind-expanding), but are rather a standard feature of dependent type theory that allows us to blur or even erase the distinction between types and terms; types are simply terms inside some universe type (more than one such type is required because otherwise we get the universe type as a member of itself, which throws up Russell-style paradoxes). Universes are an indispensable tool for such type theories, allowing one to use the useful constructions of the term-level language to define new types. The omission of universes from the earlier work was not an accident, but stems from an observation of Orton and Pitts that adding universes in the standard way in fact leads to a contradiction. This is related to a fact that not all families of fibrant types - which is to say, correct types for cubical type theory - are themselves fibrant; but if we want universes to be first class types, they must indeed be fibrant.

The solution to this is perhaps a bit surprising (although it is anticipated somewhat by earlier work by Michael Shulman), as it comes from modal logic, or more precisely, modal type theory. In particular there is a ‘global elements’ functor on cubical sets that behaves like the box modality of the intuitionistic version of a well known modal logic called S4. For this reason, techniques in type theory developed for that modal logic are applicable to that functor, namely a `dual zone’ variables context. Here all variables in one zone, called the ‘crisp’ variables, implicitly have the functor applied to them. Any term that is then substituted for a crisp variable must itself depend only on crisp variables. This notion is put to work in the definition of the ‘code’ and ‘elements’ constructions which relate types to elements of universes, as the dependencies in their definitions are required to be crisp, which precisely blocks the earlier proof of contradiction. A final argument which revolves around the interval having a property called ‘tininess’ shows that not only does the universe thus defined enjoy the properties it should have, but that it does so uniquely.

Discussing "Horn Clause Solvers for Program Verification"

(Link)

Authors: Nikolaj Bjørner (Microsoft Research Redmond), Arie Gurfinkel (Software Engineering Institute), Ken McMillan (Microsoft Research Redmond) & Andrey Rybalchenko (Microsoft Research Cambridge)

Reference: Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A. (2015). Horn Clause Solvers for Program Verification. In: Beklemishev, L., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds) Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. Lecture Notes in Computer Science, vol 9300. Springer, Cham. https://doi.org/10.1007/978-3-319-23534-9_2

Why this paper? Cited by Multiple Query Satisfiability of Constrained Horn Clauses and Parameterized Recursive Refinement Types for Automated Program Verification

This paper is a small jump away from my usual research area, based as it is on automatic program verification rather than interactive theorem proving, let alone some of my more pure interests in logic and mathematics. However it does bump up against one of my interests (Craig interpolation) and fortunately is a highly readable and not too technical survey article summarising a field of work.

Horn clauses come in various forms in this paper, but in general are a sharp constraint on the way in which logic formulae can be written down: instead of the freedom to use logical connectives wherever one desires, one must write one’s formula in a precisely specified structure. For example, all universal quantifiers might be required to be on the outside level rather than nested inside the formulae, there is a limit of one implication in the whole formulae between a ‘body’ and ‘head’ which themselves have strict rules regarding their construction, and so on. Formulae of first-order logic can be tortured until they fit the pattern required by a set of Horn clauses, albeit at some cost of time and space. Furthermore, in this paper the underlying logic is extended with an additional assertion language, usually something like a limited notion of arithmetic, which may be useful for expressing properties of programs.

The point of forcing us to write our logical statements in a highly constrained fashion is to find a compromise point between expressivity – we can talk in meaningful ways about the properties of interesting programs – and efficiency for automatic verification of these properties. After introducing the basic notions, this paper is roughly split between these two concerns. One half gives examples of various notions for turning both programs and interesting properties of these programs into Horn clauses, for example an approach based on weakest preconditions applied to the verification language Boogie. The other half looks at ways that Horn clauses can be transformed to support more successful automation. It is this half where Craig interpolation, a famous property from logical theory, intersects with the practical concerns of this paper, as a certain useful Horn clause transformation called ‘unfold’ can only be guaranteed to be sound if the underlying assertion logic enjoys the property.

Discussing "A Framework for Intuitionistic Modal Logics (Extended Abstract)"

(Link)

Authors: Gordon Plotkin and Colin Stirling (Edinburgh University)

Reference: Plotkin, Gordon, and Colin Stirling. "A framework for intuitionistic modal logics (Extended abstract)". Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK), pp. 399-406. 1986.

Why this paper? Cited by A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals, Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement, and Intuitionistic versions of modal fixed point logics

Eight years before Alex Simpson’s thesis, which I discussed on this blog just four weeks ago, comes this extremely short (8 pages in a fairly large font!) but groundbreaking paper on intuitionistic modal logics. This paper is specifically the first to look at possible world semantics, also called Kripke semantics after its inventor Saul Kripke, for such logics. I will not repeat the things I said about intuitionistic modal logics in my previous post, but rather focus on this topic of possible worlds semantics.

Classically the truth of a proposition can be calculated based on ‘truth tables’, through which logical connectives can be seen as functions from the propositions they apply to. For example, negation is the function mapping True to False and False to True. The modal connectives Box and Diamond, for necessity and possibility respectively, are not truth-functional in this way. Instead we give meaning to our new connectives by relativising truth to a set of possible worlds, in which a certain proposition might be true in some, but false in others. In fact, a mere set of worlds is not enough; in order to talk sensibly about applying modalities on top of each other, we need to know how the worlds are arranged with respect to relative notions of possibility. For example, if the world Earth-One can be imagined as possible from the world Earth-Prime, does it follow that the inhabitants of Earth-One can imagine the world Earth-Prime? If all worlds have this symmetry, this corresponds to the axiom ‘B’, which states that if a proposition holds, then it necessarily possibly holds. Piling up modalities in this style can, frankly, strain our intuitions, but possible worlds semantics makes things transparent by asking to define the relationship between worlds as part of our definition.

One cool thing about possible worlds semantics is that intuitionistic logic, the logic of constructive reasoning, can also be seen through this lens. Worlds are now viewed as ‘states of knowledge’ and moving from one world to another corresponds to gaining knowledge, for example by discovering a proof of a new mathematical theorem. This setup allows us to give sound and complete semantics for intuitionistic logic (and in particular, its implication connective) within normal mathematics.

What if we wanted to combine the two flavours of logic? Plotkin and Sterling quite correctly predicted that this could have computational significance, an ongoing subject of my own (and others’) work to this day. The aim of this paper was to work out some details of how the Kripke semantics should work for this combination, with an emphasis more on working out a technically reasonable suggestion than on making a philosophical argument. Their suggestion is to have one set of worlds with two relations, one for the modal connectives and one for intuitionistic implication. However possible worlds semantics for intuitionistic logic have the crucial property that moving between worlds cannot falsify previously established truths, but only introduce new ones. If the two relations on worlds are unrelated, this property fails, and so work needs to be done to make them harmonise. A minimal logic (Intuitionistic K, where the K stands for Kripke) is established for these semantics, and some axiomatic extensions such as the B axiom are considered.

Discussing "Categories for the Working Mathematician"

(Link)

Author: Saunders Mac Lane (University of Chicago)

Reference: Mac Lane, Saunders. Categories for the working mathematician. Second Edition. Graduate Texts in Mathematics Vol. 5. Springer-Verlag, 1998 (or for the First Edition, 1971).

Why this paper? Cited by Under Lock and Key: A Proof System for a Multimodal Logic, Groupoid-Valued Presheaf Models of Univalent Type Theory, and KZ-monads and Kan Injectivity

When I started my research career with a Master’s degree at Victoria University of Wellington under the supervision of Rob Goldblatt, this book was not quite where I got started with the fascinating world of category theory (that was Rob’s own wonderful, if somewhat idiosyncratic, Topoi), but was the working reference book I quickly moved to. When Rob and I published my first ever paper (a nice, if not exactly earth-shattering, exploration of collections of coalgebras) we cited this book for some standard definitions and results in category theory we were relying on. This was and remains a typical way to use this book – it has such canonical status that if something in one’s paper relies on something in the book, one can always safely leave its definition to a citation to Mac Lane on the understanding that reviewers and readers should have access to it, preferably in a prominent place on their bookshelf. While I have bought and acquired various reference books over the years, it remains the only one I have ever requested to receive as a Christmas present (thank you to my sister-in-law!). Its iconic status can also be seen from the fact that it is the only abstract mathematics book that I am aware of to have launched a meme, via the quote “All told, a monad in X is just a monoid in the category of endofunctors of X”:
 

Sources: 1 2 3. The word ‘just’ does a lot of work in making this quote funny. Indeed the full exposition about monoids in a category doesn’t come until the chapter after the infamous quote, so the reader could be forgiven for being a little perplexed, let alone the poor functional programmer who just wants to deal with side effects.

Mac Lane was one of the inventors (or discoverers, depending on how one feels about the ontological status of mathematics) of category theory, along with Samuel Eilenberg in 1942. There is no particular rule that the inventor of a discipline will be its best communicator, but surely it doesn’t hurt that Mac Lane maintained an overview of the field from its infancy. The original work was motivated by an attempt to better understand the notion of ‘limit’ in algebraic topology. This led them to formalise the previously informal notion of natural transformation; to get to this, one must first define functor, and to get to that, one must define category. Even though category theory can enter deep and difficult waters, and has a reputation for being hard, the definition of category is startlingly simple and general – a collection of objects, and a collection of arrows between them, obeying identity and associativity rules.

Category theory was “initially… used chiefly as a language” in Mac Lane’s telling, that is a formal language of objects and arrows, from which one can translate back and forth to the sets and elements of ‘normal’ mathematics. It still has that feeling to some extent, as learning category theory after being taught mathematics via sets can indeed feel like learning a second language as an adult. It is often claimed, correctly I think, that a second language can enrich your thinking beyond one’s ability to communicate with a different group of people, because it helps you to organise your thoughts in different ways and hence see the world in different ways. So it certainly is with category theory; armed with the basic definitions, and the knowledge that much of mathematics can be naturally viewed via objects and arrows (typically, some notion of homomorphism or structure-preserving function) one can develop category theory as a topic in its own right, bringing forward new fundamental concepts such as adjunction that do not obviously arise as fundamental when one is thinking in a different mathematical language, but once discovered can be widely and fruitfully applied. The analogy with human languages should not be overdone, of course, because for the most part human languages must be compatible with a variety of viewpoints and personalities, whereas a mathematical language can more strongly bias one to emphasise certain ways of looking at the world. With category theory, one is invited to view the mathematical world in terms of arrows (indeed, Mac Lane shows that one can formulate it without reference to objects at all), so transformations, rather than static elements, become the basis of thought and practice.

This might not be the best book to learn category theory from scratch (I haven’t done a survey of all options, but many speak highly of Awodey’s Category Theory), but once one has the basics down, it gives a clear and readable exposition of many important concepts. It is not impressive in its size and weight in the same manner as Johnstone’s Elephant, but the judicious selection of material for a relatively slim volume is impressive in its own way. It certainly still lives up to its billing as a valuable tool for the working mathematician (or, indeed, theoretical computer scientist) to consult when authors deal with some fundamental piece of category theory by citation.

Discussing "Sketches of an Elephant: A Topos Theory Compendium"

Links: Volume 1 and Volume 2

Author: Peter T. Johnstone (University of Cambridge)

Reference: Johnstone, Peter T., Sketches of an Elephant: A Topos Theory Compendium: Volume 1 and 2. Oxford University Press, 2002

Why this book? Cited by Groupoid-Valued Presheaf Models of Univalent Type Theory, KZ-monads and Kan Injectivity, and Classifying Topoi in Synthetic Guarded Domain Theory

The algorithm I follow to choose topics for this blog, where I take the most highly cited paper from my recent Google Scholar recommendations, can send me off to anything from a short conference paper to a full book. I like the variety, but of course a short blog post can only say so much about a book based on a week of reading pushed in around my other commitments; this was never more true than this week, given the monumental scale and density of these two volumes. The introduction even warns one off reading the book from start to finish; it is intended to be a tome one can dip into to find all manner of important facts in topos theory, including full proof details.

The title of the book refers to the ancient parable of the blind men and the elephant, where men touching different parts of the elephant come to different conclusions about its nature. The book is structured around sections describing the category theoretical notion of topos in different ways - as a category, as a 2-category, as a space, and as a logical theory (the latter being my main focus). The contents for a third volume are also included, covering homotopy / cohomology and mathematical universes, but more than twenty years later this is perhaps as likely to appear as the final Game of Thrones novels – but who knows?

The central definition of a topos in category theory is quite simple for something that can inspire so many pages of work, but this is in keeping with the usual nature of category theory – simple abstract definitions with many examples, which help to organise the structure of mathematical thought and provide connections between apparently unconnected areas. The distinctive concept here is that of subobject classifier, which can be seen as an object of ‘truth values’.  Classically, one can use the two element set of the Booleans True and False, but, to take a contrasting example, in the topos of trees the subobject classifier provides for an infinite-valued logic, as I discussed a few weeks ago. In any topos, the logic provided for by the subobject classifier is at least intuitionistic, but need not be classical (admitting the law of excluded middle, double negation elimination, and so on).

What do I mean by the ‘logic provided for’? To skip ahead to the logic section in the second half of the second book, a lot can be achieved without going all the way to toposes. For example, (sorted) first-order logic of the kind one might be taught in an introductory logic course can be interpreted in any Heyting category, which is a weaker definition than topos. The full power of toposes are not needed to interpret logical theories until one reaches for higher-order logic; in particular the ability to have variables ranging over subsets of a sort (more generally, type), and to sensibly use the set membership symbol ∈, requires the subobject classifier. Having said that, toposes do have their uses as an analytic tool before we get to such powerful logics, as each theory (collection of axioms) expressed with the weaker logics can be aligned to a ‘classifying topos’ which contains a universal model of the theory – a model that satisfies all and only the theorems entailed by the theory.

I should finish by mentioning one of the most stunning achievements of topos theory (to my mind; given the nature of the elephant a topologist would probably come up with something else), which is the connection of the notion of classical logic (certain toposes are Boolean, which means that their underlying logic will be classical) to the axiom of choice much discussed in mathematics. The results, rewarding one for getting 991 pages into the book (or skipping forward to them, as is more to be advised) give a description of Booleans toposes exactly in terms of the choice functions of certain of their objects, and, following Zermelo’s theorem, show that in any topos (including non-Boolean) the objects with choice functions are exactly those that are well-orderable. These results, and others around them, bring a remarkable new clarity to the connections between two of the most discussed concepts in the foundations of mathematics, classicality and choice.

Discussing "Some Properties of Fib as a Fibred 2-category"

(Link)

Author: Claudio Hermida (McGill University)

Reference: Claudio Hermida, Some properties of Fib as a fibred 2-category, Journal of Pure and Applied Algebra, Volume 134, Issue 1, 1999, Pages 83-109

Why this paper? Cited by Semantics for two-dimensional type theory and Linear Dependent Type Theory for Quantum Programming Languages

I generally try to keep the technical content of this blog relatively low; this is a bit of a challenge for a paper like this which focuses on technical development, with most applications and examples left as pointers to the literature. I will at minimum have to assume some familiarity with the mathematical field of category theory to get anywhere with this post.

This paper combines two ideas in category theory, namely fibrations and 2-categories. To get to fibrations, one can (following Chapter 1 of this PhD thesis) start with the notion of an indexed set, which can be defined as a function from a set of elements to an index set. The ‘fibres’ of a certain index are then all the elements that are mapped to that index. A fibration is the categorification of this concept – categorification is not a precise term, but is broadly the process of replacing sets with categories in one’s definitions, usually motivated by a desire for more general results. One here replaces the function between sets with a functor between categories. This move turns out to be fruitful for type theory and (typed first- and higher- order) logic because we can take our index category to be contexts and category ‘above’ to be, for example, where propositions live; the ‘fibres’ then pick out those propositions which make sense in a certain context.

What of 2-categories? One slightly amusing motivation is that sets can be considered 0-categories, ordinary categories as 1-categories, and so 2-categories are merely the categorification of the notion of a category! This makes some sense if one has spent time with categories, as one often talks not just of the categories themselves, and functors between them, but of morphisms between functors, which are called natural transformations (in fact, the historical motivation for the development of category theory was exactly to formalise the notion of natural transformation; some of the other useful terminology was invented as a by-product). The concept of 2-category then gives the general definition for a mathematical structure with that sort of three-level structure of objects, maps between objects, and maps between maps (or if not ‘the’ definition, at least a framework for such definitions, because one in fact gets a few different definitions based on how ‘lax’ or ‘strict’ one wants to be about certain equalities).

This paper’s contribution is to introduce a 2-categorical counterpart of fibrations. The paradigmatic example of such a 2-fibration turns out to be the category Fib of ordinary 1-fibrations, which is fibred over (has an appropriate functor to) the 2-category of categories. At this point one might with some justification feel one’s head start to spin, but Hermida goes on to exploit this viewpoint to prove a variety of theorems about Fib. The value of Fib, to type theory in particular, means that this paper has been steadily cited since its publication, with a modest recent uptick thanks to type theoretic interest in higher categories being driven by research in homotopy type theory.

Discussing "The Proof Theory and Semantics of Intuitionistic Modal Logic"

(Link)

Author: Alex K. Simpson (University of Edinburgh)

Reference: Simpson, Alex K. "The proof theory and semantics of intuitionistic modal logic.", PhD dissertation, University of Edinburgh (1994).

Why this paper? Cited by When programs have to watch paint dry, Wijesekera-style constructive modal logics, and Nested Sequents for First-Order Modal Logics via Reachability Rules

Computer science PhD dissertations, despite being an important part of academic life, are seldom widely read – the work is usually split into more digestible publications in journals and conference proceedings. There are exceptions, however, where the dissertation transcends merely being a stapled-together collection of papers to instead provide a comprehensive overview of a subject at a point of time. This dissertation, with its 557 citations as measured by (the sometimes slightly inaccurate) Google Scholar, is certainly an example of such.

The topic of the dissertation is the merge of intuitionistic logic and modal logic. Intuitionistic logic arose from the constructive mathematics of Brouwer, in which the notion of proof is elevated above the more mysterious notion of mathematical truth. Taking this as our basic logic requires a more restricted logic than is usually accepted, as we reject e.g. double negation elimination, as demonstrating the absence of a disproof does not entail the existence of a proof. Constructivism has become an important topic in computer science because the central concern of our discipline is that which can be constructed (via algorithm). Modal logic is the logic of possibility, necessity, and similar logical connectives. After Kripke (who recently passed away) we think of them as connectives which allow us to discuss `possible worlds’ – a certain thing may be true, but it is only necessarily true if it holds at all possible worlds.

Combining these two logics is a natural thing to do to allow modal connectives to be used in an intuitionistic setting, and has a number of computer science applications, including some that I have published on. The sticking point turns out not to be the ‘box’ operator for necessity (regarding all possible worlds), which has been translated to the intuitionistic setting without controversy many times, but rather the ‘diamond’ operator of possibility (regarding the existence of at least one possible world). Simpson’s first order of business is to survey the literature and make an argument for a particular approach to diamond, which has a range of desirable properties such as distribution over disjunction (if it is possible that A or B holds, then either it is possible that A holds, or possible that B holds).

The bulk of the dissertation revolves around structural proof theory, with natural deduction emphasised. Simpson builds the notion of possible worlds into his proof theory, with explicit requirements to show that certain worlds are possible (more technically, that one world is ‘reachable’ from another). The proof theory is shown to have good properties such as (various notions of) soundness and completeness, and strong normalisation (one can define a proof simplification procedure that is guaranteed to terminate). Most interestingly the proof theory is highly flexible, as a variety of modal logics, differentiated by different notions of the structure of possible worlds, can fit into Simpson’s framework via certain rules that reflect the semantic structure into the proof theory.

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.

Discussing "Structural Proof Theory"

(Link)

Authors: Sara Negri and Jan von Plato (University of Helsinki)

Reference: Negri, Sara, and von Plato, Jan. Structural proof theory. Cambridge University Press, 2001.

Why this book? Cited by Two-sided Sequent Calculi for FDE-like Four-valued Logics and Proof Theory for Intuitionistic Temporal Logic

There has been an unplanned delay to the blog, as two weeks ago there were not enough new recommendations appearing in Google Scholar to recommend any ‘classic papers’ for me to review via their citations, and then one week ago we got this book, which took me a small while to track down. I therefore expect to post twice this week.

A `structural’ proof is one that proceeds via a set of inference rules that forces one to arrange one’s proof in a tree-like structure, using only a limited set of inference rules and axioms. These inference rules generally reflect the logical connectives used to state the proposition one is trying to prove.  For example, to prove a conjunction one `branches’ to prove each side of the conjunction separately. This may seem a mundane or obvious notion, but is actually very young with respect to the long history of logic, originating with Gerhard Gentzen in the 1930s. The structural approach allows one to study the space of proofs for a given logic as an object of mathematical interest in its own right (hence, proof theory) and can help with finding proofs.

The two important systems for structural proof are natural deduction and sequent calculus, both originating with Gentzen. Natural deduction is intended to reflect the natural way in which one reasons logically, and is an important concept in computer science due to its relationship with types: according to the Curry-Howard isomorphism, programs with a given type can be viewed as natural deduction proofs of a certain proposition, and vice versa. Sequent calculus is a slightly less natural notion where one works on `sequents’ which allow one to manipulate one’s premises as well as one’s conclusion(s). This turns out to be an ideal setting in which to study the space of all proofs for a logic, and can support automated proof search and help to demonstrate that non-theorems are not provable. While the two approaches differ, they also have many similarities; for example, both have a notion of an algorithm (called normalisation or reduction for natural deduction, and cut-elimination for sequent calculus) that automatically simplifies unnecessarily complex or indirect proofs.

This book is a careful development of various notions of natural deduction and sequent calculus for classical, intuitionistic, and intermediate logic, including propositions, predicates, equality, and ‘nonlogical rules’ that give one access to the axioms of various parts of logic. Full proof details are given throughout the book, a number of new results are presented alongside the classic results, and care is taken to place ideas in their historical context. The high level of detail make this a less breezy read than, say, Girard’s Proofs and Types, but it is in invaluable tool to anyone working in the area.

Discussing "Separation Logic: A Logic for Shared Mutable Data Structures"

(Link)

Author: John C. Reynolds (Carnegie Mellon University)

Reference: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, 2002, pp. 55-74, doi: 10.1109/LICS.2002.1029817.

Why this paper? Cited by On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs, Compositional Verification of Interacting Systems Using Event Monads, and Semantic Cut Elimination for the Logic of Bunched Implications and Structural Extensions, Formalized in Coq.

How can we be sure that the programs we write do what they’re supposed to? An answer from the late 1960s is Hoare logic, which gives a formal relationship between programs and specifications. Crucially, Hoare logic can be used in a modular way, in the sense that parts of the program can be reasoned about separately, rather than demanding that an entire program must be reasoned about all at once – a completely impossible task even for some relatively small programs.

Traditional Hoare logic becomes unusable in the face of languages (for example, C) that allow the direct manipulation of memory within the code. Because there is nothing to stop two different program variables pointing to the same physical piece of memory, a manipulation that only seems to effect one variable may also effect another, even if that variable exists in some long distant piece of code. However, the direct manipulation of memory (and potential for ‘sharing’ that this creates) can be extremely useful, as can be seen in various examples in this paper by Reynolds. For example, we see a list reversal where instead of creating a new list that is a reversal of the input, we take the memory-saving approach of reversing by swapping values within the list.

This paper introduces the term separation logic, but mostly reports and summarises previous work by Reynolds and others (primarily Peter O’Hearn, Samin Ishtiaq, and Hongseok Yang, with inspiration from Rod Burstall and David Pym). The key innovation of this group is to change the logical language in which specifications can be stated. A separating conjunction ∗ joins the usual list of logical operators, with a proposition of form P ∗ Q holding if P and Q hold of entirely separate parts of memory. This allows modular reasoning to be restored via a frame rule that says that a true statement about a fragment of one’s code remains true if put in the context of other memory, so long as that extra memory remains separate from the fragment in question. Another connective called separating implication also joins the party, along with a constant stating that no memory is in use, and some syntax to allow one to talk about the content of memory. The paper goes on to present a treasure trove of examples, extensions, and directions for the future, with a heavy emphasis on the application of the logic to a variety of data structures and program constructs.

Discussing 'Homotopy Type Theory: Univalent Foundations of Mathematics'

 (Link)

Author: The Univalent Foundations Program (Institute for Advanced Study)

Why this paper? Cited by Internal Strict Propositions Using Point-Free Equations, Probabilistic Programming and Multiverse Models of Type Theory, and Contextual Algebraic Theories: Generic Boilerplate beyond Abstraction (Extended Abstract).

The first thing to note about this e-book is its unusual authorship - it was put together by a collective of 27, along with various visitors and students, working together at the IAS in Princeton across a special year of study. The most famous participant was the Fields Medal (roughly equivalent to a Nobel Prize for mathematics) winner Vladimir Voevodsky, who sadly passed away a few years ago, aged just 51.

I will not attempt to summarise a 490 page book in a short blog post, but I can give some sense of the flavour of this work. It concerns a foundation of mathematics known as type theory. A foundation of mathematics might sound like an abstruse thing, and sometimes it can be, but it is essentially a description of what things mathematicians are able to talk about, and the rules they must follow to construct valid arguments about them. Nailing this down precisely is becoming increasingly vital, as we grow to understand that some mathematics (for example, proofs about software) can get too complex to fully trust a pen-and-paper proof by a human. The alternative is to have a somewhat simple-minded but indefatigable computer program check every step of a proof for error; for this to be possible, we must be precise about what language the program should be able to read and inferences it should be prepared to accept – in other words, our foundation of mathematics. Type theory is an approach to foundations that naturally lends itself to this sort of automated proof checking, as it involves working with syntax not too far from that of a programming language (although one of the arguments of this book is that one can de-formalise type theory to present proofs in a style more natural for human mathematicians as well).

This book introduces a new (at the time) direction in type theory known as homotopy type theory. The motivation is to get better behaviour for proofs of equality in type theory, with particular attention to applications in mathematical areas such as topology and category theory. The standard approaches to equality in type theory are well understood but rather blunt. The intensional approach only identifies functions (for example) when they have the same definition, up to some automatic simplifications a computer can easily run, and so will often not identify functions that produce the same output on all inputs, because their definitions differ – this is a reasonable approach to equality, but rather more limited than the use of equality in ordinary mathematics. The extensional approach, which ignores the details of definitions, lacks appealing computational properties. The insight that led to this book was that we can get a more nuanced notion of equality if we think of objects in our type theory as points in spaces, with equalities as paths between them modulo continuous deformation, a point of view taken from the mathematical field of homotopy theory. This concept takes some out of their mathematical comfort zone, but the idea has more to offer than better support for formalisation of homotopy theory itself (although it does offer that); borrowing the notion of path gives rise to a new notion of type theory in which equality has more interesting properties, and in particular does not collapse to mere definitional equality or something impossible to compute with.

The main new technical gains of taking the homotopy point of view into type theory are the univalence axiom, and higher inductive types. The univalence axiom essentially says that one can treat an equivalence (roughly, a mathematical proof that two objects are essentially ‘the same’), the same way one treats the type-theoretic construct of equality. Practically, this means that once one has proved an equivalence between two mathematical definitions, one can treat them as identical for all purposes, even switching back and forth during a proof to use whichever definition is most convenient at a given time, without risk of error. This mirrors standard informal mathematical practice but is sometimes considered an ‘abuse of notation’, i.e. something that should really be avoided in a fully rigorous development. With homotopy type theory, it is correct and completely formal to work like this. Higher inductive types are a general approach to constructing mathematical objects which include equalities as part of their inductive definition, and are vital for work formalising homotopy theory, but are also shown to be useful to other applications, for example to define the notion of colimit in category theory, and that of quotients of sets.

Discussing 'Notions of Computation and Monads'

(Link)

Author: Eugenio Moggi (University of Edinburgh)

Reference: Information and computation 93.1 (1991): 55-92

Why this paper? Cited by Normalization for Fitch-Style Modal Calculi, Probabilistic Programming and Multiverse Models of Type Theory, and Denotational Semantics of General Store and Polymorphism  in my Google Scholar recommendations.

This famous paper suggested the use of the important but rather abstract category theoretic concept known as a monad to assist with reasoning about programming languages and programs that feature side effects. A side effect is an aspect of computation that cannot be easily described as a final output of a deterministic program, variously because it refers to output that happens during computation (such as printing to the screen), a failure to create an output (such as crashing with an error), or an opportunity for something (such as a user) to interact with the computation. The monad (typically written T) of choice depends on which type of side effect(s) one wishes to incorporate. Having chosen the monad, we can draw a distinction between the values of a type A - the sort of thing one can use as an input - and the type TA of computations of type A. This fine-grained distinction allows one to formally discuss the side effects, and not merely the result, of a program of interest.

The style in which Moggi presents his monads are at least as important as the concept itself, as he suggests introducing them, with new notation and equational rules, into a lambda calculus, both as a ‘metalanguage’ for reasoning about programming languages with side effects, and as a programming language in its own right. This has been influential in the use of monads in programming in Haskell  and other languages.