# PPLV Research Seminar

The PPLV group hosts an (approximately) weekly invited research seminar on Thursdays. Upcoming talks are listed on this page, and are open to any interested UCL student or staff member. An archive of past talks from 2012 to 2018 can be found here.

If you are interested in giving a research seminar, please contact Simon Docherty in the first instance.

# Upcoming Seminars

Time / date: | Thursday 1st August 2019 / 2-3pm |
---|---|

Speaker: | Alexandra Silva and Tobias Kappé (UCL) |

Location: | Room 405, 66-72 Gower Street |

Title: | Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time |

Abstract: | Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa’s axiomatization of Kleene Algebra. |

# Recent Talks

Time / date: | Thursday 25th July 2019, 2-3pm |
---|---|

Speaker: | Aquinas Hobor (National University of Singapore) |

Location: | Room 405, 66-72 Gower Street |

Title: | A Functional Proof Pearl: Inverting the Ackermann Hierarchy |

Abstract: | We implement in Gallina a hierarchy of functions that calculate the upper inverses to the hyperoperation/Ackermann hierarchy. Our functions run in Theta(b) for inputs expressed in unary, and O(b^2) for inputs expressed in binary (where b = bitlength). We use our inverses to define linear-time functions---Theta(b) for both unary- and binary-represented inputs---that compute the upper inverse of the diagonal Ackermann function A(n) and show that these functions are consistent with the usual definition of the inverse Ackermann function alpha(n). |

Time / date: | Thursday 18th July 2019 / 2-3pm |
---|---|

Speaker: | Cristina Matache (Oxford) |

Location: | Room 405, 66-72 Gower Street |

Title: | A Sound and Complete Logic for Algebraic Effects |

Abstract: | Title: A Sound and Complete Logic for Algebraic Effects I will talk about definitions of program equivalence, for a language with algebraic effects in the style of Plotkin and Power. Program equivalence is a long-standing problem in computer science, made more difficult by the presence of higher-order functions and algebraic effects. In this talk I will present a logic whose formulas represent properties of effectful programs. The satisfaction relation of the logic induces a notion of program equivalence. Notably, the induced equivalence coincides with contextual equivalence (which equates programs with the same observable behaviour) and also with an applicative bisimilarity. This is joint work with Sam Staton which appeared at FOSSACS 2019. https://link.springer.com/content/pdf/10.1007%2F978-3-030-17127-8_22.pdf |

Time / date: | Thursday 27th June 2019 / 2-3pm |
---|---|

Speaker: | Didier Galmiche (LORIA) |

Location: | Room 405, 66-72 Gower Street |

Title: | An Epistemic Resource Logic |

Abstract: | We present an epistemic resource logic, based on Boolean BI, in which the epistemic modalities are parametrized on agents' local resources. The new modalities can be seen as generalizations of the usual epistemic modalities. The logic combines Boolean BI's resource semantics with epistemic agency. We illustrate the use of the logic with an example about access control. We also present a labelled tableaux calculus that is sound and complete w.r.t. the resource semantics. Joint work with Pierre Kimmel (LORIA) and David Pym (UCL). |

Time / date: | Thursday 13th June 2019 / 2-3pm |
---|---|

Speaker: | Andrei Popescu (Middlesex) |

Location: | Room 405, 66-72 Gower Street |

Title: | Some results on the logical foundations of proof assistants based on Higher-Order Logic |

Abstract: | Verification tools, and proof assistants prominently among them, are moving on to become the guardians of the galaxy in terms of reliable computing systems and proofs of mathematical results. But who is guarding the guardians? In particular, do we have a good understanding of the logical foundations of the proof assistants in current use? In recent years, several logical fallacies have been discovered in well-maintained and heavily used proof assistants, which have led to inconsistency (the proof of False). Most of these problems were hiding in the definitional mechanisms, and have to do with non-terminating recursion. In this talk, I will present our journey from discovering and correcting such a fallacy in a major proof assistant to producing a detailed proof that the corrected logic is now consistent. I also present a result that is relevant to the foundation of several proof assistants: that definitions in Gordon-style Higher-Order Logic are "safe" in a very strong sense, which implies conservativity (and of course consistency). (Joint work with Ondrej Kuncar) |

Time / date: | Thursday 23rd May, 2019 / 2-3pm |
---|---|

Speaker: | Paul Brunet (UCL) |

Location: | Room 405, 66-72 Gower Street |

Title: | Bracket Algebras: a nominal theory of interleaved scopes |

Abstract: | Nominal techniques have received a lot of attention in recent years, as they describe in a simple yet precise manner phenomena related to variable renaming, like alpha-equivalence, scopes, locality... However, they seem to suffer from two shortcomings: they are not yet able to handle interleaved scopes, and do not apply well to relational semantics of programs. In this talk I will describe an ongoing project to provide an algebraic treatment of the semantics of programming languages which contain explicitly allocation and de-allocation binders, inspired by previous work of Gabbay, Ghica and Petris?an. I will present the initial setup, defining a notion of alpha-equivalence of traces, and briefly describe how this may be extended to regular languages. I will present some decidability results we obtained, and hint at future investigations. Most of these developments have been formalised in Coq. This is joint work with Alexandra Silva and Daniela Petri?an. |

Time / date: | Monday 13th May, 2019 / 2-3pm |
---|---|

Speaker: | Dan Ghica (University of Birmingham) |

Location: | Room 405, 66-72 Gower Street |

Title: | The Next 700 Abstract Machines |

Abstract: | We propose a new core calculus for programming languages with extrinsic effects, interpreted using a graph-rewriting abstract machine. The intrinsic calculus only deals with the most general structural aspects of programming languages: variable binding, name binding, and thunking. Everything else, including function abstraction and application, must be provided as extrinsic operations with associated rewrite rules. The graph representation yields new natural concepts of 'locality' and 'robustness' for equational properties and reduction rules, which enable novel equational reasoning techniques for languages with effects. Moreover, the abstract machine framework also allows precise reasoning about the time and space cost of computation. (joint work with Koko Muroya and Todd Waugh Ambridge) |

Time / date: | Thursday 25th April 2019, 2pm-3pm |
---|---|

Speaker: | Jurriaan Rot (UCL/Radboud) |

Location: | Room 405, 66-72 Gower Street |

Title: | Coalgebra Learning via Duality |

Abstract: |
Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. We generalise learning from automata to a large class of state-based systems, using the theory of coalgebras. The approach relies on the use of logical formulas as tests, based on a dual adjunction between states and logical theories. This allows us to learn, e.g., labelled transition systems. Joint work with Clemens Kupke and Simone Barlocco. |

Time / date: | Thursday 11th April 2019, 2pm-3pm |
---|---|

Speaker: | Maaike Zwart (Oxford) |

Location: | Room 405, 66-72 Gower Street |

Title: | Don't Try This At Home: No Go Theorems for Distributive Laws |

Abstract: |
Beck's distributive laws provide sufficient conditions under which two monads can be composed, and monads arising from distributive laws have many desirable theoretical properties. Unfortunately, finding and verifying distributive laws, or establishing if one even exists, can be extremely difficult and error-prone. We develop general-purpose techniques for showing when there can be no distributive law between two monads. Two approaches are presented. The first widely generalizes ideas from a counterexample attributed to Plotkin, yielding general-purpose theorems that recover the previously known situations in which no distributive law can exist. Our second approach is entirely novel, encompassing new practical situations beyond our generalization of Plotkin's approach. It negatively resolves the open question of whether the list monad distributes over itself. Our approach adopts an algebraic perspective throughout, exploiting a syntactic characterization of distributive laws. This approach is key to generalizing beyond what has been achieved by direct calculations in previous work. We show via examples many situations in which our theorems can be applied. This includes a detailed analysis of distributive laws for members of an extension of the Boom type hierarchy, well known to functional programmers. (Joint work with Dan Marsden) |

Time / date: | Thursday 21st March 2019, 2pm-3pm |
---|---|

Speaker: | Julian Nagele (QMUL) |

Location: | Room 405, 66-72 Gower Street |

Title: | Automated Confluence Analysis of Rewriting |

Abstract: | Rewriting is a simple yet Turing complete model of computation. It is the process of transforming objects in a step-wise fashion, where typically the objects are expressions in some formal language, and the transformations are given by a set of directed equations. A fundamental notion in rewriting is confluence, which guarantees uniqueness of results, i.e., that the equations in question specify a partial function. Generalising confluence to multiple sets of equations yields the related notion of commutation, which can be used to study correctness of program transformations. Although undecidable in general, much work has been spent on confluence analysis, with automatic tools under active development. The achievements in confluence research have enabled the annual confluence competition where these tools try to establish/refute confluence. In this talk I will provide an overview of automated confluence analysis of rewriting, discussing some key concepts in the underlying theory, and the current state of tool support. |

Time / date: | Thursday 14th March 2019, 2pm-3pm |
---|---|

Speaker: | James Cheney (University of Edinburgh/Turing Institute) |

Location: | G01, 66-72 Gower Street |

Title: | Incremental relational lenses |

Abstract: |
Lenses are a popular approach to bidirectional transformations, a generalisation of the view update problem in databases, in which we wish to make changes to source tables to effect a desired change on a view. However, perhaps surprisingly, lenses have seldom actually been used to implement updatable views in databases. Bohannon, Pierce and Vaughan proposed an approach to updatable views called relational lenses, but to the best of our knowledge this proposal has not been implemented or evaluated to date. We propose incremental relational lenses, that equip relational lenses with change-propagating semantics that map small changes to the view to (potentially) small changes to the source tables. We also present a language-integrated implementation of relational lenses and a detailed experimental evaluation, showing orders of magnitude improvement over the non-incremental approach. Our work shows that relational lenses can be used to support expressive and efficient view updates at the language level, without relying on updatable view support from the underlying database. Joint work with Rudi Horn and Roly Perera. Incremental relational lenses. Proc. ACM Program. Lang. 2, ICFP, Article 74 (July 2018), 30 pages. DOI: https://doi.org/10.1145/3236769 |

Time / date: | Thursday 7th March 2019, 2:30pm-3:30pm |
---|---|

Speaker: | Alessio Lomuscio (Imperial) |

Location: | GS01, 66-72 Gower Street |

Title: | Advances in the Verification of Multi-Agent Systems |

Abstract: |
Multi-agent Systems (MAS) are distributed autonomous systems in which the components, or agents, act autonomously in order to reach private or common goals. MAS have been used as a paradigm to realise a wide number of applications ranging from autonomous systems and robotics to services, electronic assistants, and beyond. Logic-based specifications for MAS typically do not refer only to the agents’ temporal evolution, but also to their knowledge, strategic abilities, and other AI-inspired primitives. I will begin by reporting algorithms for symbolic model checking against epistemic and strategic specifications. I will highlight potential speedups of these techniques via a number of techniques including symmetry reduction, parallel approaches, and SAT-based methods. I will demonstrate MCMAS, an open-source BDD-based model checker supporting these specification languages. A case study concerning the verification of diagnosability and fault-tolerance of an autonomous underwater vehicle will be discussed. I will then consider the case of MAS where the number of agents is unbounded and cannot be determined at design time. This is a typical assumption in robotic swarms and recent internet of things applications. In view of solving this, I will report our approach to the parameterised model checking problem. While this is generally undecidable, I will present results that establish sufficient conditions for determining a cut-off of a MAS, i.e., the number of agents that need to analysed for verifying a MAS composed of any number of components. I concluded by presenting applications to the verification of related notions, such as emergence. |

Time / date: | Thursday 21st February 2019, 3pm-4pm |
---|---|

Speaker: | Derek Dreyer (MPI-SWS) |

Location: | Room 405, 66-72 Gower Street |

Title: | UCL CS Distinguished Lecture: RustBelt: Logical Foundations for the Future of Safe Systems Programming |

Abstract: | Rust is a new systems programming language, sponsored by Mozilla, that promises to overcome the seemingly fundamental tradeoff in language design between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this talk, I will present RustBelt (http://plv.mpi-sws.org/rustbelt), the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem. After reviewing some essential features of the Rust language, I will describe the high-level structure of the RustBelt verification and then delve into detail about the secret weapon that makes RustBelt possible: the Iris framework for higher-order concurrent separation logic in Coq (http://iris-project.org). I will explain by example how Iris generalizes the expressive power of O'Hearn's original Concurrent Separation Logic in ways that are essential for verifying the safety of Rust libraries. I will not assume any prior familiarity with Concurrent Separation Logic or Rust. This is joint work with Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Hoang-Hai Dang, Jan-Oliver Kaiser, and the rest of the Iris team. |

Time / date: | Thursday 14th February 2019, 3pm-4pm |
---|---|

Speaker: | Siddharth Krishna (NYU) |

Location: | Room 405, 66-72 Gower Street |

Title: | Verifying Concurrent Search Structure Templates |

Abstract: | Concurrent separation logics have had great success reasoning about concurrent data structures. This success stems from their application of modularity on multiple levels, leading to proofs that are decomposed according to program structure, program state, and individual threads. Despite these advances, it remains difficult to achieve proof reuse across different data structure implementations. For the large class of search structures, we demonstrate how one can achieve further proof modularity by decoupling the proof of thread safety from the proof of structural integrity. We base our work on the template algorithms of Shasha and Goodman, that dictate how threads interact but abstract from the concrete layout of nodes in memory. Building on our recent flow framework [POPL '18] of compositional abstractions and the separation logic ReLoC/Iris, we show how to prove contextual refinement for template algorithms, and how to instantiate them to obtain multiple verified implementations. We demonstrate our approach by formalizing three concurrent search structure templates, based on link, give-up, and lock-coupling synchronization, and deriving implementations based on B-trees, hash tables, and linked lists. Our proofs are mechanized and partially automated using the Coq proof assistant and the deductive verification tool GRASShopper. Not only does our approach reduce the proof complexity, we are also able to achieve significant proof reuse. |