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.