# PPLV Research Seminar

The PPLV group hosts an (approximately) weekly research seminar. 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 Timo Lang in the first instance.

# Upcoming Talks

Time / date: | Feb 15th 2024 / 1-2pm |
---|---|

Speaker: | George Kaye (University Of Birmingham) |

Location: | Seminar Room 405 |

Title: | A Fully Compositional Theory of Sequential Digital Circuits |

Abstract: | Digital circuits, despite having been studied for nearly a century and used at scale for about half that time, have until recently evaded a fully compositional theoretical understanding, in which arbitrary circuits may be freely composed together without consulting their internals. Recent work remedied this theoretical shortcoming by showing how digital circuits can be presented compositionally as morphisms in a freely generated symmetric traced category. However, this was done informally, and in this talk I will show how we have refined and expanded on the previous work in several ways, culminating in the presentation of three sound and complete semantics for digital circuits: denotational, operational and algebraic. |

# Recent Talks

Time / date: | Jan 25th 2024 / 1-2pm |
---|---|

Speaker: | Carlos Olarte (Université Sorbonne Paris Nord) |

Location: | Seminar Room 405 |

Title: | Process-as-formula interpretation: Subexponentials, focusing and multimodalities in concurrent systems |

Abstract: | We show how the processes-as-formulas interpretation, where computations and proof-search are strongly connected, can be used to specify different concurrent behaviors as logical theories. The proposed interpretation is parametric and modular, and it faithfully captures behaviors such as: Linear and spatial computations, epistemic state of agents, and preferences in concurrent systems. The key for this modularity is the incorporation of multimodalities in a resource aware logic, together with the ability of quantifying on such modalities. Our tight adequacy results rely on a focusing discipline controlling the proof search process, and we show that one step of logical reasoning corresponds exactly to one step of computation. (Joint work with Elaine Pimentel and Vivek Nigam). |

Time / date: | June 8th 2023 / 1-2pm |
---|---|

Speaker: | Prakash Panangaden (McGill University, University of Edinburgh) |

Location: | Seminar Room 405 |

Title: | Quantitative Equational Reasoning |

Abstract: | We develop a quantitative analogue of equational reasoning which we call quantitative algebra. We define an equality relation indexed by rationals which we think of as capturing approximate equality. This allows one to capture metric reasoning in a framework similar to equational reasoning. The theory of equational logic and universal algebra extends smoothly to this metric setting. We have several interesting examples where we have a quantitative equational theory whose free algebras correspond to well known structures. In each case we have finitary and continuous versions. Since its introduction in 2016 the theory has evolved rapidly and many new examples have been discovered. I will present this topic from scratch so it should be widely accessible. This is joint work with Giorgio Bacci, Radu Mardare and Gordon Plotkin. |

Time / date: | January 20th 2023 / time tba |
---|---|

Speaker: | Tim Fernando (Trinity College Dublin) |

Location: | tba |

Title: | Finite-state predication and temporal deformation |

Abstract: | The difference between stative verbs such as OWN and non-stative verbs such as BUY is cashed out against transitions by finite automata. Adopting the perspective of grammar induction, the challenge is to infer regularities (for example, automata) by generalizing over observations, encoded in strings (commonly extracted from runs of an automaton). The observations are understood to have bounded granularities and refinements, which are put in a category of signatures that index a logical system called an institution (Goguen & Burstall 1992). Amalgamation (gluing) is complicated by compression, an instance of what David Mumford calls domain warping --- one of four universal types of deformations Mumford highlights within Ulf Grenander's Pattern Theory. Instances of the three other deformation types are also discernible over regular expressions, describing, up to bounded granularities, time, conceived as change recorded in strings (roughly, comic strips). |

Time / date: | Thursday 8th December 2022 / 2.30pm |
---|---|

Speaker: | John Baez (UC Riverside) |

Location: | 26 Bedford Way, room 305 |

Title: | Compositional Modelling with Decorated Cospans |

Abstract: | Decorated cospans are a general framework for working with open systems with the help of double categories. We explain this framework and illustrate it with the example of stock-flow diagrams. These diagrams are widely used in epidemiology to model the dynamics of populations. Although tools already exist for building these diagrams and simulating the models they describe, we have created a software package called StockFlow which uses decorated cospans to overcome some limitations of existing software. Our approach enables the composition of stock-flow diagrams, and cleanly separates their syntax from the semantics they can be assigned. We have implemented three forms of semantics, including one where stock-flow diagrams are mapped to ordinary differential equations. We have also created a web-based graphical user interface for StockFlow that requires no knowledge of category theory or programming to use. This is joint work with Xiaoyan Li, Sophie Libkind, Nathaniel Osgood, Evan Patterson, Long Pham and Eric Redekopp. |

Time / date: | November 24th 2022 / 1-2pm |
---|---|

Speaker: | Sanjaye Ramgoolam (Queen Mary University London) |

Location: | room 1.02, Malet Place Engineering Building |

Title: | Graphs, Invariants and Gaussianity in Matrix data, with applications to computational linguistics. |

Abstract: | I describe low-dimensional vector representations of large matrix data, derived using constructions from permutation invariant random matrix theory (PIRMT). The vector spaces are constructed using directed graphs corresponding to invariants of the permutation symmetry. They are equipped with geometries arising from random matrix theory and statistics. Approximate Gaussianity in the matrix data is quantified using a framework similar to the application of quantum field theory (QFT) in particle physics. This is made possible by mathematical analogies between QFT and random matrix theory, which can be viewed as zero dimensional QFT. The low dimensionality of the graph-based vector representations is motivated by the approximate Gaussianity. I describe concrete applications of the vector representations in the context of data from computational linguistics. Predicting word relations involving synonyms, antonyms, hypernyms and hyponyms are some of the computational tasks in these applications. I discuss some similarities and differences between these perspectives from PIRMT and those underlying traditional applications of random matrix theory in data sciences. This talk is based on an interdisciplinary collaboration between theoretical physicists and computer scientists. |

Time / date: | Friday 18th November 2022 / 1-2pm |
---|---|

Speaker: | Jas Semrl (UCL) |

Location: | 66 Gower Street, G01 |

Title: | Represenable and diagonally representable weakening relation algebras |

Abstract: | A relation over some poset is a weakening relation if and only if the ordering acts as a two-sided identity. This is motivated by the weakening rule in sequent calculi. In joint work with Peter Jipsen, we present some results and speculations about the theory of [diagonally] representable relation algebras. Analogous to relation algebras, we define triangular presentations of weakening relation algebras (showing an interesting connection to relevance logic) as well as various representation games. Finally, we work towards axiomatising the abstract class of weakening relation algebras. |

Time / date: | Friday 11th November 2022 / 1-2pm |
---|---|

Speaker: | Robin Hirsch (UCL) |

Location: | 66 Gower Street, G01 |

Title: | Algebras of Binary Relations, Representations, Games. |

Abstract: | We consider sets of binary relations over some base, closed under a given set of natural operations, for example, boolean operations, an identity element, converse, composition, kleene star and maybe others, like demonic composition. My talk is a tutorial-seminar, reviewing techniques and results that evolved over decades, and surveying some slightly more recent results. |

Time / date: | Friday 4th November 2022 / 1-2pm |
---|---|

Speaker: | Alex Gheorghiu (UCL) |

Location: | 66 Gower Street, G01 |

Title: | Introduction to Proof-theoretic Semantics |

Abstract: | Traditionally, semantics within logic and informatics is denotationalist --- that is, the meaning of a object within a system is defined according to its interpretation in some abstract structure, such as a model. A contrasting view is inferentialism, according to which the meaning of an object within a system is determined by its (inferential) behaviour in that system. In this way, inferentialism is a particular instantiation of the `meaning is use' principle. A mathematical actualization of the inferentialist view is proof-theoretic semantics, in which inference is understood with respect to a proof system. In short, proof-theoretic semantics is to inferentialism as model-theoretic semantics is to denotationalism. |

Time / date: | Friday 28th October 2022 / 1-2pm |
---|---|

Speaker: | James Brotherston (UCL) |

Location: | 66 Gower Street, G01 |

Title: | tba |

Abstract: | tba |

Time / date: | Friday 21st November 2022 / 1-2pm |
---|---|

Speaker: | Ian Lo Kin (UCL) |

Location: | 66 Gower Street, G01 |

Title: | A Model of Anaphoric Ambiguities using Sheaf Theoretic Quantum-like Contextuality and BERT |

Abstract: | Ambiguities of natural language do not preclude us from using it and context helps in getting ideas across. They, nonetheless, pose a key challenge to the development of competent machines to understand natural language and use it as humans do. Contextuality is an unparalleled phenomenon in quantum mechanics, where different mathematical formalisms have been put forwards to understand and reason about it. In this paper, we construct a schema for anaphoric ambiguities that exhibits quantum-like contextuality. We use a recently developed criterion of sheaf-theoretic contextuality that is applicable to signalling models. We then take advantage of the neural word embedding engine BERT to instantiate the schema to natural language examples and extract probability distributions for the instances. As a result, plenty of sheaf-contextual examples were discovered in the natural language corpora BERT utilises. Our hope is that these examples will pave the way for future research and for finding ways to extend applications of quantum computing to natural language processing. |

Time / date: | Thursday 7th July 2022 / 10.30am-12pm |
---|---|

Speaker: | Jose Meseguer (U. Illinois / King's College) |

Location: | zoom or 66 Gower Street, G01 |

Title: | Building Correct-by-Construction Systems with Formal Patterns |

Abstract: | Formal patterns are formally specified generic solutions to commonly occurring computational problems that are correct by construction. Being generic, a formal pattern applies, not just to a single system, but to a typically infinite class of systems that satisfy some requirements. Application of a formal pattern to a system satisfying the formal pattern’s input requirements results in a new system with new functionality that is correct by construction. Such correctness takes the form of an assume-guarantee property: assuming the original system meets the formal pattern’s input requirements, then application of the formal pattern to such a system is guaranteed to enjoy specific correctness properties. The notion of formal pattern can be best expressed in the computational logic of a declarative programming language, so that a program is a theory in such a logic. I will use rewriting logic and the Maude language to illustrate the main ideas. Mathematically, a formal pattern is a theory transformation P that transforms the theory T specifying an input system, perhaps with some additional parameters p, into a new theory P(T,p) specifying the new correct-by-construction system generated by P. I will explain the notion of formal pattern and will give examples of formal patterns to build systems in different areas such as: (i) cyber-physical systems, (ii) distributed systems, (iii) secure systems, (iv) theorem proving, and (v) probabilistic verification. |

Time / date: | Tuesday 28th June 2022 / 4-5pm |
---|---|

Speaker: | Stefan Zetzsche (UCL) |

Location: | zoom or 66 Gower Street, G01 |

Title: | Guarded Kleene Algebra with Tests: Automata Learning |

Abstract: | Guarded Kleene Algebra with Tests (GKAT) is the fragment of Kleene Algebra with Tests (KAT) that arises by replacing the union and iteration operations of KAT with predicate-guarded variants. GKAT is more efficiently decidable than KAT and expressive enough to model simple imperative programs, making it attractive for applications to e.g. network verification. In this paper, we further explore GKAT's automata theory, and present GL*, an algorithm for learning the GKAT automaton representation of a black-box, by observing its behaviour. A complexity analysis shows that it is more efficient to learn a representation of a GKAT program with GL* than with Angluin's existing L* algorithm. We implement GL* and L* in OCaml and compare their performances on example programs. |

Time / date: | Friday 24th June 2022 / 2-3pm |
---|---|

Speaker: | Tim Button (UCL) |

Location: | zoom or 66 Gower Street, G01 |

Title: | MOON theory: Mathematical Objects with Ontological Neutrality |

Abstract: | The iterative notion of set starts with a simple, coherent story, and yields a paradise of mathematical objects. But it does not present an attractive mathematical ontology: it seems daft to say that every mathematical object is "really" some (pure) set. My goal, in this paper, is to explain how we can inhabit the set-theorist's paradise of mathematical objects whilst remaining ontologically neutral. I start by presenting a very general template for telling stories about entities which are found stage-by-stage. The iterative notion of set can be introduced with just such a story; but so can plenty of other notions. I introduce the idea of a MOON, as a formal theory which formalizes some (any) such story. A MOON+ is then the formalization of some (any) such story, plus the additional claim "there is no last stage". I prove a result. Theorem. All MOON+s are synonymous. Consequently, all MOON+s are synonymous with a theory which articulates the iterative notion of set. So: MOON+s can deliver the set-theorist's paradise of mathematical objects. But, since different MOON+s have different (apparent) ontologies, we can be ontologically neutral. |

Time / date: | Friday 17th June 2022 / 2-3pm |
---|---|

Speaker: | Manuele Bujorianu (UCL) |

Location: | zoom or 66 Gower Street, G01 |

Title: | Model checking in real life environments |

Abstract: | Today software is often deployed in real harsh physical environments. Climate change makes this challenge acute. The safety and performability problems get new formulations in this new context. We present a concept of model checking tuned to this setting. This is called stochastic reachability analysis and it emerges from reliability analysis in engineering. |

Time / date: | Friday 27th May 2022 / 2-3pm |
---|---|

Speaker: | Gijs Wijnholds (Utrecht University) |

Location: | zoom or 66 Gower Street, G01 |

Title: | Compositional Models of Vector-based Semantics: From Theory to Tractable Implementation |

Abstract: | I report on recent developments in our current research project `A composition calculus for vector-based semantic modelling with a localization for Dutch’. Starting out from (and building upon) the Thursday talk by Michael Moortgat, I discuss briefly the concept of a multi-modal Lambek Calculus for capturing linguistic constituency structure and dependency structure in a single logic. Then, I discuss some of the theoretical challenges regarding a compositional treatment of natural language, treading on the fine line between derivational and lexical semantics in the case of (parasitic) gapping. If time permits I show how in such cases a graphical language can be used to visualise proofs. Afterwards I move on to tractable implementations and current work in progress. Specifically I discuss how we have built a type extractor and parser that allow us to map arbitrary (Dutch) text to types and proofs. On the practical side I will talk about how such systems can be used/compared against state of the art deep learning methods for sentence representation. I end with some open problems/questions. |

Time / date: | Friday 6th May 2022 / 2-3pm |
---|---|

Speaker: | Timo Eckhardt (UCL) |

Location: | zoom or 66 Gower Street, G01 |

Title: | Modelling Forgetting in Dynamic Epistemic Logic |

Abstract: | In this talk I will present a model changing operation that represents loss of information for a group of agents in a multi-agent epistemic modal logic. This method is based on an idea of minimal forgetting in which only the least possible information is forgotten. A method is developed to identify this minimal information and worlds will be created to correspond to these minimal changes. Lastly, This will be used to give a logical operator corresponding to the idea of "forgetting that". |

Time / date: | Friday 8th April 2022 / 2-3pm |
---|---|

Speaker: | Timo Lang (UCL) |

Location: | zoom or 66 Gower Street, G01 |

Title: | Cut Elimination and Cut Restriction |

Abstract: | The last decades of structural proof theory have seen a rise of new proof systems, all extending Gentzen’s famous sequent calculus: Hypersequent Calculi, Labelled Sequent Calculi, Deep Inference Systems… A common goal of these extended systems is to prove cut elimination theorems for nonclassical logics where cut elimination is not possible in the sequent calculus. An alternative to this search for new formalisms is to remain in the sequent calculus, and establish a bound on the instances of cuts which are needed to capture a given target logic. For some reason this path is much less travelled. I will discuss some joint work with Agata Ciabattoni and Revantha Ramanayake in this direction, which uses two different syntactic methods: First, projecting cutfree proofs in an extended system (such as the hypersequent calculus) onto proofs in the sequent calculus, and second, generalizing Gentzen’s method of cut elimination. The talk will include a mini-introduction to structural proof theory. |

Time / date: | Friday 1st April 2022 / 2-3pm |
---|---|

Speaker: | Will Smith (UCL) |

Location: | zoom or 66 Gower Street, G01 |

Title: | Deterministic operational semantics for probabilistic programming languages |

Abstract: | In this session, I’ll review trace semantics for probabilistic programs (without conditioning), and discuss what the natural relationship between operational semantics and denotational semantics should be for probabilistic programs, especially in the case where ’sampling’ is accomplished via deterministic means. I’ll focus specifically on the application of statistical inference, giving informal examples of the types of reasoning our arguments are intended to formalise, and emphasize the application of theories of approximate sampling to providing operational semantics for probabilistic programs with conditioning. |

Time / date: | Friday 25th March 2022 / 2-3pm |
---|---|

Speaker: | Fredrik Dahlqvist (UCL) |

Location: | zoom or Gordon Street 22, G.11 |

Title: | The linear operator semantics of probabilistic programs. |

Abstract: | In this tutorial I will present a semantics for probabilistic programs in terms of linear operators. Mathematically, this is the natural universe in which to talk about probabilistic transition systems - both discrete and continuous - and it therefore makes sense to target this universe when defining a denotational semantics for probabilistic programming languages. I will describe the basic theory and how both higher-order functions and Bayesian inference can be interpreted in this framework. The focus of the tutorial will be on the discrete case, which amounts to manipulating matrices, but I will also sketch some of the mathematics behind the general case. This tutorial will cover joint work with Vincent Danos, Ilias Garnier and Dexter Kozen. |

Time / date: | Friday 18th March 2022 / 2-3pm |
---|---|

Speaker: | David Sprunger (University of Birmingham) |

Location: | zoom or Gordon Street 22, G.11 |

Title: | Functorial String Diagrams for Reverse-Mode Automatic Differentiation |

Abstract: | In this talk, I will describe hierarchical string diagrams, an extension of monoidal string diagrams to monoidal closed categories inspired by functorial boxes [Mellies, 2006]. Leveraging the ability of these diagrams to represent function abstraction, we will combine this with reverse differential categories [Cockett et al, 2019] to explore the higher-order reverse-mode AD algorithm proposed by Pearlmutter and Siskind in 2008. In particular, we produce a transformation on hierarchical string diagrams which produces a new string diagram which is the derivative of the original. Joint work with Mario Alvarez-Picallo, Dan Ghica and Fabio Zanasi |

Time / date: | Friday 11th March 2022 / 2-3pm |
---|---|

Speaker: | Cole Comfort (University of Oxford) |

Location: | zoom or Gordon Street 22, G.11 |

Title: | Graphical Symplectic Algebra |

Abstract: | Inspired by the graphical calculi for affine and linear relations, we give presentations in terms of string diagrams for the props of linear/affine Lagrangian/coisotropic relations. Owing to their symplectic nature, these props give semantics for various classes of mechanical systems; notably stabilizer quantum circuits, as well as passive electrical circuits, depending on wich base field is chosen. We show that there are two constructions, both intepreted as "adding discarding", which produce coisotropic relations from Lagrangian relations. By splitting an idempotent in coisotropic relations, one obtains a two sorted prop: the original sort corresponds to the mechanical system and the new one corresponds to the linear system. In the case of stabilizer circuits, the former is the quantum system, and the latter is the classical system. In the case of stabilizer circuits, the new sort is interpreted as carrying the measured value of a current or a voltage. We also give a presentation for this two sorted prop. (This paper builds on previous work with Aleks Kissinger https://arxiv.org/abs/2105.06244) |

Time / date: | Friday 25th February 2022 / 2-3pm |
---|---|

Speaker: | Mehrnoosh Sadrzadeh (UCL) |

Location: | zoom or Gordon Street 22, G.11 |

Title: | Copying and permutation in substructural logics |

Abstract: | In 1958 Lambek proposed the logic of a residuated monoid to reason about syntax of natural language. This logic was amongst the first substructural logics. It did not have contraction nor weakening, properties that indeed were not necessary for fixed word order languages. Apart from difficulties in generalizing this logic to free word order languages, such as Sanskrit and Latin, they also failed to model discourse structure, i.e. structures that go beyond sentential boundaries, for instance in the simple discourse "John slept. He snored." In this talk, I will show how endowing Lambek Calculus with controlled modalities overcomes the problem. I will also go through the vector semantics of such logics and show interesting applications to natural language tasks and recent adventures on the possibilities of running the tasks on Quantum computers. This is joint work with Lachlan, Hadi and Ian. |

Time / date: | Friday 18th February 2022 / 2-3pm |
---|---|

Speaker: | Alex Gheorghiu (UCL) |

Location: | zoom or Gordon Street 22, G.11 |

Title: | Semantics ex Proof and Refutation |

Abstract: | By using a perspective on logic known as Reductive Logic, we develop a method for synthesising the model-theoretic semantics (MTS) for a logic by analysing how its proof-search behaviour differs from the proof-search behaviour in another logic for which one already has an MTS. This technique enables a new method for proving soundness and completeness (using co-induction on proof-search attempts) that allows us to work with entailment and provability directly (i.e., allows us to bypass truth). The technology enabling the method is the use of `algebraic constraints’ for which we have developed a general theory with applications within both the theory and practice of logic. |

Time / date: | Friday 10th February 2022 / 2-3pm |
---|---|

Speaker: | Luca Reggio (UCL) |

Location: | online |

Title: | Game comonads: towards an axiomatic theory of resources |

Abstract: | Game comonads, introduced by Abramsky, Dawar et al. in 2017, provide a categorical approach to finite model theory. A basic instance of this framework allows to recover, in a purely syntax-free way, the following ingredients: the Ehrenfeucht-Fraïssé game, fragments of first-order logic with bounded quantifier rank (and variations thereof), and the combinatorial parameter of tree-depth. Other instances cover, e.g., k-pebble games and bisimulation games, and the corresponding logic fragments and combinatorial parameters. After an introduction to game comonads, I shall present an axiomatic framework which captures the essential common features of these constructions. This is based on the notion of arboreal cover, a resource-indexed family of adjunctions with some ``process category'' - which unfolds relational structures into treelike forms, allowing resource parameters to be assigned to these unfoldings. Beyond this basic level, a landscape is beginning to emerge, in which structural features of the resource categories and comonads are reflected in degrees of tractability of the corresponding logic fragments. If time permits, I will then discuss an application of game comonads to homomorphism counting results in finite model theory. The prototypical homomorphism counting result is Lovasz' theorem (1967), stating that graphs A and B are isomorphic if and only if, for every graph C, the number of homomorphisms from C to A is the same as the number of homomorphisms from C to B. Game comonads yield uniform proofs of Lovasz' theorem and more recent results of Dvorak (2010) and Grohe (2020), as well as a novel homomorphism counting result in modal logic. |

Time / date: | Friday 28th January 2022 / 2-3pm |
---|---|

Speaker: | Elaine Pimentel (UCL) |

Location: | online |

Title: | A quest for uniformity and meaning |

Abstract: | Close your eyes and, from the cloud of subjects/interests/views that have been part of your research so far, pick two words that better characterize your work. What would they be? In my case, the answer is: "uniform" and "meaning". In fact, most of my efforts have been devoted to finding uniform ways of describing/proving/reasoning about different logical objects. And, in doing so, I try to get from such objects a meaning that makes sense to me. In this talk, I will present some uniform views on proof systems. Starting with the cut rule, which formalizes the use of lemmas in mathematics, Dale Miller showed me that it is all about dualities. And that this can be uniformly captured using linear logic (LL). Then Carlos Olarte helped me realize that formulas in LL can, in fact, be interpreted as concurrent processes, and we investigated the computational meaning of multi-modalities in LL (SELL). With Björn Lellmann we studied other kinds of modalities in LL, going below the "S4" flavor (SDML). This picture got complete when Timo Lang showed us the dynamic of SELL, where proofs are put into play (and there is a cost for that!). There are some interesting open questions that I would like to address in this first part of the talk. For example (a) what is the computational interpretation of SDML?; (b) what is the play of costs in SELL's cut-elimination? (c) how about non-normal modalities and open systems? The second part will be devoted to the discussion of modalities, but in the ecumenical (classical/intuitionistic) setting. With Sonia Marin we have proposed a proof system where (normal) modalities can co-exist in piece. But then, what does it tell us about extensions? For that, we need to understand well the role of axioms and atomic formulas. And this will be the final theme of discussion. |

Time / date: | Friday 21st January 2022 / 2-3pm |
---|---|

Speaker: | Robin Piedeleu (UCL) |

Location: | online |

Title: | An Axiomatisation of Finite-State Automata as String Diagrams |

Abstract: | Based on joint work with Fabio Zanasi, I'll introduce a fully diagrammatic approach to finite-state automata. In this setting, we'll see how we can derive a complete equational theory for language equivalence, with two notable features: 1) the proposed axiomatisation is finite; 2) the Kleene star is a derived concept, as it can be decomposed into more primitive diagrammatic blocks. I will try to keep the category theory to a minimum. |

Time / date: | Wednesday 12th January 2022 / 4-5pm |
---|---|

Speaker: | Wojciech Różowski (UCL) |

Location: | online |

Title: | Formally verified derivation of an executable and terminating CEK machine from call-by-value λp̂-calculus |

Abstract: | Throughout the development of functional programming languages, one of the most researched topics is their implementation. A common approach is specifying their semantics in terms of abstract machines, first-order deterministic transition systems. It is known that abstract machines can be derived from calculi with explicit substitutions through well-understood program transformations. Formalising them in dependently-typed programming languages allows for obtaining machines proven to be correct. This work introduces the Agda formalisation of an executable and terminating CEK machine, obtained from simply typed call-by-value λp̂-calculus. The novel contributions have been the successful extension of Swierstra’s previous research on the Krivine machine to a broader case, as well as providing elegant Tait-style proof of Strong Normalisation of call-by-value λp̂-calculus. |

Time / date: | Thursday 9nd December 2021 / 4-5pm |
---|---|

Speaker: | Linpeng Zhang (UCL) |

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

Title: | Quantitative Strongest Post |

Abstract: | We present a novel strongest-postcondition-style calculus for quantitative reasoning about non-deterministic programs with loops. Whereas existing quantitative weakest pre transformers allow reasoning from a given initial state about the value of a quantity after program execution, quantitative strongest post allows reasoning from a given final state about the value that a quantity had before program execution. We demonstrate how strongest post enables reasoning about the flow of quantitative information through programs. Similarly to weakest liberal preconditions, we too develop a quantitative strongest liberal post. As a byproduct, we obtain the entirely unexplored notion of strongest liberal postconditions and show how these foreshadow a potential new program logic - partial incorrectness logic - which would be a more liberal version of O’Hearn’s recent incorrectness logic. |

Time / date: | Thursday 2nd December 2021 / 4-5pm |
---|---|

Speaker: | Tobias Kappé (ILLC, University of Amsterdam) |

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

Title: | Leapfrog: Certified Equivalence for Protocol Parsers |

Abstract: | Because network protocol parsers have to meet strict performance targets, they are typically subjected to a wide range of optimizations, applied by programmer and compiler alike. These optimizations complicate the code, and by extension its verification. We present Leapfrog, a Coq-based framework for verifying the equivalence of parsers, including reference and optimized implementations of the same protocol. By combining symbolic representations, up-to techniques, and integration with off-the-shelf SMT solvers, Leapfrog is able to automatically verify many common parser optimizations, and scales up to do translation verification of a third-party parser compiler. |

Time / date: | Thursday 25th November 2021 / 4-5pm |
---|---|

Speaker: | Leo Lobski (UCL) |

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

Title: | Partition functor for effect algebras: a model of quantum measurements |

Abstract: | One of the most striking features of quantum mechanics is its notion of a measurement: in general, an individual measurement of a system gives information about a proper subset of all the physical properties that could be observed in theory (and not about the entire system). In this way, epistemology (what can be observed by measuring) gets decoupled from ontology (the whole system that is supposedly out there). A natural question then arises: are all the measurements collectively sufficient (in theory) to fully determine the whole system? In order to maintain an objective notion of the physical reality, one would hope the answer to this question to be affirmative. In this talk, I will formulate the question as (conjectured) essential injectivity of the so-called 'partitions of unity functor' from the category of effect algebras to the category of posets. After this, setting aside the physical motivation, I will provide mathematical evidence towards the truth of the conjecture by discussing two special cases in which the conjecture is known to hold: Boolean algebras and finite MV-algebras. The talk is based on my MSc thesis. |

Time / date: | Thursday 18th November 2021 / 4-5pm |
---|---|

Speaker: | Lachlan McPheat (UCL) |

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

Title: | Vector Space Semantics for Lambek Calculus with Soft Subexponentials |

Abstract: | We develop a vector space semantics for Lambek Calculus with Soft Subexponentials, apply the calculus to construct compositional vector interpretations for parasitic gap noun phrases and discourse units with anaphora and ellipsis, and experiment with the constructions in a distributional sentence similarity task. As opposed to previous work, which used Lambek Calculus with a Relevant Modality the calculus used in this paper uses a bounded version of the modality and is decidable. The vector space semantics of this new modality allows us to meaningfully define contraction as projection and provide a linear theory behind what we could previously only achieve via nonlinear maps. |

Time / date: | Thursday 11th November 2021 / 4-5pm |
---|---|

Speaker: | Daphne Wang (UCL) |

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

Title: | Quantum-like contextuality in natural language |

Abstract: | Most words in the English language can hold different interpretations depending on the context they are found in; for example, book in the sentence the book is on the table is a physical object whilst in the book is interesting, the same word correspond to a more abstract concept which has some informational content. Although this idea is widely used in computational linguistics, the nature of the influence from the context on sense disambiguation is not known, and in fact the notion of context itself is generally kept vague and inconsistent throughout the literature. In a completely different field, the notion of context also plays a major role in the formulation of quantum mechanics, as physical values are thought to be (measurement)-context dependent. In particular, this phenomenon gave rise to a wide range of mathematical formalisms which studies the influence of the context on observed probability distributions. What we have shown in previous work is that quantum-like contextuality does arise in natural language when considering ambiguous phrases. In more recent work, we are addressing the issues with uses of the different formalisms and are developing a more general theory about context-dependent language understanding. |

Time / date: | Tuesday 26th October 2021 / 1-2pm |
---|---|

Speaker: | Samson Abramsky(UCL) |

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

Title: | Relating Structure and Power |

Abstract: | There is a remarkable divide in the field of logic in Computer Science, between two distinct strands: one focussing on semantics and compositionality (``Structure''), the other on expressiveness and complexity (``Power''). It is remarkable because these two fundamental aspects are studied using almost disjoint technical languages and methods, by almost disjoint research communities. We believe that bridging this divide is a major issue in Computer Science, and may hold the key to fundamental advances in the field.In this talk, we describe a novel approach to relating categorical semantics, which exemplifies the first strand, to finite model theory, which exemplifies the second. |

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. |

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. |