Discussing "A Modal Analysis of Staged Computation"

(Link)

Authors: Rowan Davies and Frank Pfenning (Carnegie Mellon University)

Reference: Davies, Rowan, and Frank Pfenning. "A modal analysis of staged computation". Journal of the ACM (JACM) 48.3 (2001): 555-604.

Why this paper? Cited by A Fibrational Approach to Multiplicative Additive Indexed Linear Logic and Proofs and Refutations for Intuitionistic and Second-Order Logic

This week we have some work I know and love (although I think I’ve spent more time with the shorter conference version, published in 1996). The central idea is for a programmer to state using their type system in which order (expressed as stages) their program will execute. This would allow various optimisations to be applied automatically at compile time. We achieve this via a new type constructor, written ☐. Code of type ☐A is understood as unevaluated code of that type. For example, there is always a function from ☐A to A, which works by evaluating the code.

The cool thing here for a logician interested in the Curry-Howard isomorphism between proofs and programs is that this new type-former behaves exactly like the necessity, or box, modality of the well known modal logic S4 (more precisely, the intuitionistic version of this logic, without the possibility, or diamond, modality). For example, necessitation (a standard feature of all normal modal logics) corresponds to the ability to treat an arbitrary closed program as code, which does not hold of programs with free variables. So this paper, developing as it does lambda calculi for this box, is both a contribution to a particular programming language problem and to the proof theory of an important modal logic.

There are a number of different calculi developed in this paper, with the most important split between the dual context and context stack approaches. This nicely prefigures more recent work in modal lambda calculus, which supports the conclusion that while other approaches work for specific modal logics, these are the two approaches powerful enough to work for a large variety of modal logics; see here for a modern view of the first approach, and a paper of mine for the second. Another split is between the calculi that hew closely to the simply typed lambda calculus and (although this is not proved, it is fairly clear) are guaranteed to terminate, versus the ‘Mini-ML’ variations that achieve Turing completeness via general fixed points, at the cost of muddying the relationship with logic.

Given the context stack approach is close to my heart, I’ll make some more specific comments on this. Without getting distracted by bike shedding I'll briefly note that I do prefer the older term for this approach, Fitch-style (named in honour of work in proof theory by Frederic Fitch) over the coinage of Kripke-style here (Saul Kripke’s famous ‘possible worlds’ semantics should correspond to any reasonable proof theory, although admittedly Fitch’s approach feels closest to this semantics). The basic idea is that use of our Box modality corresponds to navigating through various layers of contexts; this is a wonderfully general idea and not fixed to the particular logic S4.

One interesting feature of S4 is that ☐…☐A is logically equivalent to ☐A for any number of boxes. My work has shown that if we are willing to allow all boxed types to further be isomorphic (true for many applications, but perhaps not appropriate for this work) we can significantly simplify the calculus of this paper. This works by removing the need for natural number indices to track how many layers of contexts are being popped at a given point of the program, and hence removing the need for ‘modal structural transformations’ in the reduction relation that are needed to relabel indices at various points. This actually contradicts the assertion in this paper that indices are necessary because of a certain ‘coherence’ problem; in fact that problem can be shown to resolve (the proof of this is not that easy), so the indices are in fact only necessary to preserve, if desired, the generality of having ☐…☐A be possibly non-isomorphic (genuinely different) to ☐A.

Discussing "Scalable Verification of Probabilistic Networks"

(Link)

Authors: Steffen Smolka (Cornell University), Praveen Kumar (Cornell University), David M. Kahn (Carnegie Mellon University), Nate Foster (Cornell University), Justin Hsu (University of Wisconsin), Dexter Kozen (Cornell University), and Alexandra Silva (University College London)

Reference: Smolka, Steffen, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva. "Scalable verification of probabilistic networks." In PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 190-203. 2019.

Why this paper? Cited by A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests and Lilac: a Modal Separation Logic for Conditional Probability

I built this blog around the idea of discoverability via Google Scholar both of new papers and, via their citations, influential older papers. Google Scholar generally does an excellent job of this (far better than the new wave of AIs with their tendency to hallucinate literature) but nothing is perfect, and the recommendations from this week are perhaps partly caused by misunderstanding that the word ‘guarded’, which is used a lot in some of my papers, is also used, but in a completely different way, in certain other papers. Still, the paper I got served by my self-imposed algorithm, while not exactly in my wheelhouse, is interesting enough so long as I don’t dive too deep into the technicalities.

This paper describes a system call McNetKAT, which is a grand pileup of acronyms: Mc for ‘Markov chain’, Net for ‘Network’, KA for ‘Kleen Algebra’, and ‘T’ for ‘(with) Tests’. The basic idea is to build capability for automatic verification on top of the programming language ProbNetKAT (Prob for ‘Probabilistic’), a small imperative language that allows one to specify the topology of a network and the policy for moving packets through it. The support for probability helps capture cases “from uncertainty about the inputs, to expected loads, to likelihood of device and link failures” that might effect networks. One can attempt to prove that the network program is fully correct, by showing that is equivalent to a magic network that teleports each packet to its correct destination, but the probabilities really come into play when you show a certain network program improves on another, in the sense that where both succeed they agree on their treatment of packets, but one is less likely to fail than another according to a given failure model on links or switches.

The ‘Mc’ comes into play because a new semantics is presented based on stochastic matrices / Markov chains, a notion of probabilistic transition system. These semantics are proved to be equal to the existing semantics in the literature, but are more amenable to automation. Programs are compiled into their semantics, and then passed to the linear algebra solver UMFPACK. It is shown that this treatment performs well against an alternative route involving compilation into the language of the probabilistic model checker PRISM, and against the (admittedly, more expressive) system Bayonet.

Discussing "The Lean Theorem Prover (System Description)"

(Link)

Authors: Leonardo de Moura (Microsoft Research Redmond)), Soonho Kong (Carnegie Mellon University), Jeremy Avigad (Carnegie Mellon University), Floris van Doorn (Carnegie Mellon University), and Jakob von Raumer (Carnegie Mellon University)

Reference: de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J. (2015). The Lean Theorem Prover (System Description). In: Felty, A., Middeldorp, A. (eds) Automated Deduction - CADE-25. CADE 2015. Lecture Notes in Computer Science(), vol 9195. Springer, Cham. https://doi.org/10.1007/978-3-319-21401-6_26

Why this paper? Cited by Encoding Dependently-Typed Constructions into Simple Type Theory and A Type-Based Approach to Divide-and-Conquer Recursion in Coq

Lean is something of a new kid on the block in the world of interactive theorem proving, coming out just 10 years ago, compared to 34 years for Coq and 36 for Isabelle. Nonetheless it has clearly had impact; for example this year’s CPP (Certified Programs and Proofs) conference, which I had the privilege to be a member of the program committee for, by my count had 7 of 25 accepted papers using Lean.

This short conference paper gives a brief and high-level description of the aims and design principles of the new theorem prover. It is neither a tutorial (see pdf) nor in-depth description of the nitty gritty of the implementation (for which see e.g. here). It does, perhaps, give some sense of why developing a new prover was thought to be desirable rather than simply using the established technologies, although it is rather polite and implicit about any comparisons with other provers. Lean, which like Coq is based on Martin-Löf dependent type theory, has a few features emphasised: its small trusted code base, its support for different proving styles (declarative à la Isabelle, or imperative-style tactics to generate proof terms), its flexible framework for supporting automation and talking to other software, its user interface, and its relatively fast speed and support for parallelism. Homotopy type theory is highlighted as one of the motivating application areas. The bulk of the paper is an informal description of the elaboration algorithm, which compiles definitions and proofs written in various styles down to the proof terms that the small trusted kernel can accept.

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.