• Elaine Pimentel has been elected the chair of the LA committee of the Association for Symbolic Logic and the treasurer of ACM SIGLOG. Both terms end in 2025.
• Paul Wilson, Dan Ghica and Fabio Zanasi's paper "String diagrams for non-strict monoidal categories" has been accepted for publication in the proceedings of Computer Science Logic (CSL) 2023.
• Mario Alvarez Picallo, Dan Ghica, David Sprunger, Fabio Zanasi's paper "Functorial String Diagrams for Reverse-Mode Automatic Differentiation" has been accepted for publication in the proceedings of Computer Science Logic (CSL) 2023.

• Paul Wilson and Fabio Zanasi's paper "Categories of Differentiable Polynomial Circuits for Machine Learning" has been accepted for a Keynote presentation at ACT 2022.
• Leo Lobski and Fabio Zanasi's paper "String Diagrams for Layered Explanations" has been accepted for publication in the proceedings of ACT 2022.
• Tao Gu, Robin Piedeleu, and Fabio Zanasi's paper "A Complete Diagrammatic Calculus for Boolean Satisfiability" has been accepted for publication in the proceedings of MFPS 2022.
• Stefan Zetzsche, Alexandra Silva and Matteo Sammartino's paper "Guarded Kleene Algebra with Tests: Automata Learning" has been accepted for publication in the proceedings of MFPS 2022.
• Wojciech Rozowski, Tobias Kappé, Todd Schmid and Alexandra Silva's work "Probabilistic Guarded Kleene Algebra with Tests" has been accepted for a presentation at VeriProp 2022.

• Mario Alvarez Picallo, Dan Ghica, David Sprunger and Fabio Zanasi's paper "Rewriting for Monoidal Closed Categories" has been accepted for publication at the 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022).
• Paul Wilson and Fabio Zanasi's paper "Categories of Differentiable Polynomial Circuits for Machine Learning" has been accepted for publication at the 15th International Conference on Graph Transformation (ICGT 2022).

• Sonia Marin, Dale Miller, Elaine Pimentel and Marco Volpe's paper "From axioms to synthetic inference rules via focusing" has been accepted for publication at the Annals of Pure and Applied Logic.
• Luca Reggio joins the group as a research fellow on Abramsky's EPSRC project "Resources in Computation": welcome Luca!
• Rafal Stefanski joins the group as a research fellow on Abramsky's EPSRC fellowship project "Resources in Computation": welcome Rafal!

• Mehrnoosh Sadrzadeh has been awarded a Royal Academy of Engineering Senior Fellowship to start in March 2022. The title is "Engineered Mathematics for Modelling Typed Structures (EMMTyS)", sponsored by Quantinuum and BBC.

• Paul Wilson and Fabio Zanasi's paper (with coauthors Geoff Cruttwell, Bruno Gavranovic, and Neil Ghani) "Categorical foundations of gradient-based learning" has been accepted for publication in the proceedings of ESOP 2022.
• Linpeng Zhang and Benjamin Kaminski's paper "Quantitative Strongest Post" has been accepted at OOPSLA 2022.

• Fabio Zanasi's paper (with coauthors Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski) "String Diagram Rewrite Theory I: Rewriting with Frobenius Structure" has been accepted for publication in the Journal of the ACM.

• Stefan Zetzsche, Gerco van Heerdt and Alexandra Silva's paper (with coauthor Matteo Sammartino) "Canonical automata via distributive law homomorphisms" has been accepted at SYCO 8.
• Robin Piedeleu's paper (with coauthor Guillaume Boisseau) "Graphical Piecewise-Linear Algebra " has been accepted at SYCO 8.

• James Brotherston, Paul Brunet, Nikos Gorogiannis and Max Kanovich's paper "A compositional deadlock detector for Android Java" has been accepted at ASE 2021.
• Fredrik Dahlqvist and Renato Neves' paper "An Internal Language for Categories Enriched over Generalised Metric Spaces" has been accepted at CSL 2022.
• Linpeng Zhang has been awarded the Best Italian Master Thesis in Theoretical Computer Science Award for his M.Sc. dissertation on "Some intensional versions of Rice's Theorem" by the Italian chapter of the European Association for Theoretical Computer Science (EATCS-IT Council).

• Todd Schmid and Fredrik Dahlqvist's paper "How to write a coequation" has been accepted at CALCO 2021.
• Stefan Zetzsche, Gerco van Heerdt and Alexandra Silva's paper (with coauthor Matteo Sammartino) "Canonical automata via distributive law homomorphisms" has been accepted at MFPS 2021.

• Fredrik Dahlqvist's paper (with coauthors George Constantinides, Zvonimir Rakamaric and Rocco Salvia) "Rigorous Roundoff Errors Analysis in Probabilistic Floating-Point Computations" has been accepted at CAV 2021.
• Benjamin Lucien Kaminski's paper (with coauthors Kevin Batz, Mingshuai Chen, Joost-Pieter Katoen, Christoph Matheja and Philipp Schröer) "Latticed k-Induction with an Application to Probabilistic Programs by Kevin Batz, Mingshuai" has been accepted at CAV 2021.
• Todd Schmid and Alexandra Silva's paper (with coauthors Tobias Kappé and Dexter Kozen) "Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness" has been accepted at ICALP 2021.
• Linpeng Zhang's paper (with coauthors Paolo Baldan and Francesco Ranzato) "A Rice's Theorem for Abstract Semantics" has been accepted at ICALP 2021.

• Robin Piedeleu and Fabio Zanasi's paper "A String Diagrammatic Axiomatisation of Finite-State Automata" won the EATCS Best Paper Award, for the best theory paper at ETAPS (European Joint Conferences on Theory and Practice of Software), awarded by the European Association for Theoretical Computer Science (EATCS).
• Diana Costa's paper (with coauthor Manuel A. Martins) "Non-dual modal operators as a basis for 4-valued accessibility relations in Hybrid logic" has been accepted at the Journal of Logical and Algebraic Methods in Programming.
• Mehrnoosh Sadrzadeh got a Discovery to Use funding for a project titled "Similarity-Based Media Recommendation" in collaboration with BBC R&D.

• Benjamin Kaminski has been awarded the prestigious Ackermann Award for his Ph.D. dissertation on "Advanced Weakest Precondition Calculi for Probabilistic Programs" which he defended in February 2019. The Ackermann Award is an annual award by the EACSL (European Association of Computer Science Logic) and is given to an outstanding dissertation in the area “Logic in Computer Science”. More details can be found here.

• Robin Piedeleu and Fabio Zanasi's paper "A String Diagrammatic Axiomatisation of Finite-State Automata" has been accepted for publication at FoSSaCS 2021.
• Alexander Gheorghiu and Sonia Marin's paper "Focused Proof-search in the Logic of Bunched Implications" has been accepted for publication at FoSSaCS 2021.
• Gerco van Heerdt, Tobias Kappé, Jurriaan Rot and Alexandra Silva's paper "Learning Pomset Automata" has been accepted for publication at FoSSaCS 2021.
• Benjamin Kaminski's paper (with coauthors Alejandro Aguirre, Gilles Barthe, Justin Hsu, Joost-Pieter Katoen, and Christoph Matheja) "A Pre-expectation Calculus for Probabilistic Sensitivity" has been awarded Distinguished Paper at POPL 2021.
• Benjamin Kaminski's paper (with coauthors Lutz Klinkenberg, Kevin Batz, Joost-Pieter Katoen, Joshua Moerman and Tobias Winkler) "Generating Functions for Probabilistic Programs" has been awarded Best Paper at LOPSTR 2020.

• Estibaliz Fraca joins the group as a research fellow on the IRIS project: welcome Esti!

• Linpeng Zhang joins the group as a PhD student, supervised by Benjamin Kaminski and Alexandra Silva: welcome Linpeng!
• Benjamin Kaminski's paper (with coauthors Kevin Batz, Joost-Pieter Katoen, and Christoph Matheja) "Relatively Complete Verification of Probabilistic Programs: An Epressive Language for Expectation-based Reasoning" has been accepted for publication at POPL 2021.
• Benjamin Kaminski's paper (with coauthors Alejandro Aguirre, Gilles Barthe, Justin Hsu, Joost-Pieter Katoen, and Christoph Matheja) "A Pre-expectation Calculus for Probabilistic Sensitivity" has been accepted for publication at POPL 2021.

• Louis Parlant, Jurriaan Rot, Alexandra Silva and Bas Westerbaan's paper "Preservation of Equations by Monoidal Monads" has been accepted for publication at MFCS 2020.
• Benjamin Kaminski's paper (with coauthors Lutz Klinkenberg, Kevin Batz, Joost-Pieter Katoen, Joshua Moerman and Tobias Winkler) "Generating Functions for Probabilistic Programs" has been accepted for publication at LOPSTR 2020.
• Tiago Ferreira joins the group as a research assistant: welcome Tiago!
• Tobias Kappé, Gerco van Heerdt and Louis Parlant have all passed their PhD vivas with minor corrections: congratulations Tobias, Gerco and Louis!

• Peter O'Hearn will give the keynote talk, titled "Formal Reasoning and the Hacker's Way" at this year's SOAP, which is co-located with PLDI 2020. The conference will be held virtually and instructions on attendance can be found here.
• Jana Wagemaker, Paul Brunet, Simon Docherty, Tobias Kappé, Jurriaan Rot and Alexandra Silva's paper "Partially Observable Kleene Algebra" has been accepted for publication at CONCUR 2020.
• Paul Wilson and Fabio Zanasi's paper "Reverse Derivative Ascent: A Categorical Approach to Learning Boolean Circuits" has been accepted for publication at ACT 2020.
• Fabio Zanasi and Alexandra Silva have been awarded a three year grant by the EPSRC for their project "Nominal String Diagrams" with Dan Ghica from University of Birmingham. Congratulations Fabio and Alexandra!

• Tao Gu, Alexandra Silva and Fabio Zanasi's paper "Hennessy-Milner Results for Probabilistic PDL" has been accepted for publication at MFPS 2020.
• Bas Westerbaan's paper (with coauthors Kenta Cho and John van de Wetering) "Dichotomy between deterministic and probabilistic models in countably additive effectus theory" has been accepted for publication at QPL 2020.

• Alexandra Silva will co-chair CAV 2021 next year: congratulations Alexandra!
• Benjamin Kaminski's paper (with coauthor Arnd Hartmanns) "Optimistic Value Iteration" has been accepted for publication at CAV 2020.
• Benjamin Kaminski's paper (with coauthors Kevin Batz, Sebastian Junges, Joost-Pieter Katoen and Christoph Matheja) "PrIC3: Property Directed Reachability for MDPs" has been accepted for publication at CAV 2020.
• James Brotherston and Diana Costa's paper (with coauthors Aquinas Hobor and John Wickerson) "Reasoning over Permissions Regions in Concurrent Separation Logic" has been accepted for publication at CAV 2020.
• Maria Schett's paper (with coauthors Elvira Albert, Pablo Gordillo and Albert Rubio) "Synthesis of Super-Optimized Smart Contracts using Max-SMT" has been accepted for publication at CAV 2020.
• Byron Cook's paper (with coauthors John Backes et al) "Stratified Abstraction of Access Control Policies" has ben accepted for publication at CAV 2020.
• Bas Westerbaan's paper (with coauthor Tobias Fritz) "The Universal Property of Infinite Direct Sums in C?-Categories and W?-Categories" has been published in Applied Category Theory this month.
• Bas Westerbaan's paper (with coauthors Abraham Westerbaan and John van de Wetering) "A characterisation of ordered abstract probabilities" has been accepted for publication at LICS 2020.
• Christoph Hasse's paper (with coauthors Georgina Bumpus, Stefan Kiefer, Paul-Ioan Stoienescu and Jonathan Tanner) "On the Size of Finite Rational Matrix Semigroups" has been accepted for publication at ICALP 2020.
• Paul Brunet and David Pym's paper "Pomsets with Boxes: Protection, Separation and Locality in Concurrent Kleene Algebra" has been accepted for publication at FSCD 2020.

• Benjamin Lucien Kaminski's paper (with coauthors Martin Grohe, Joost-Pieter Katoen and Peter Lindner) "Generative Datalog with Continuous Distributions" was accepted for publication at PODS 2020.
• Benjamin Lucien Kaminski's tutorial (with co-presenters Joost-Pieter Katoen and Christoph Matheja) "Verifying Probabilistic Programs" was accepted for presentation at QEST 2020.
• Max Kanovich's paper (with coauthors Stepan Kuznetsov, Vivek Nigam and Andre Scedrov) "Soft subexponentials and multiplexing" has been accepted for publication at IJCAR 2020.

• Tobias Kappé and Alexandra Silva's paper (with coauthors Steffen Smolka, Nate Foster, Justin Hsu and Dexter Kozen) "Guarded Kleene algebra with tests: Verification of uninterpreted programs in nearly linear time" was awarded Distinguished Paper at this year's POPL: congratulations!
• Fabio Zanasi's paper (with coauthors Facundo Carreiro, Alessandro Facchini and Yde Venema) "The power of the weak" was published in ACM Transactions on Computational Logic.
• Benjamin Lucien Kaminski joins the group as a lecturer: welcome Benjamin!
• Billy Smith joins the group as a PhD student: welcome Billy!

• Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker and Fabio Zanasi's paper "Concurrent Kleene algebra with observations: From hypotheses to completeness" has been accepted for publication at FoSSaCS 2020.
• Gerco van Heerdt, Jurrian Rot and Alexandra Silva's paper (with coauthor Clemens Kupke) "Learning weighted automata over principal ideal domains" has been accepted for publication at FoSSaCS 2020.
• Fabio Zanasi and Robin Piedeleu's paper (with coauthors Filippo Bonchi and Pawel Sobocinski) "Contextual Equivalence for Signal Flow Graphs" has been accepted for publication at FoSSaCS 2020.

• Tobias Kappé and Alexandra Silva's paper (with coauthors Steffen Smolka, Nate Foster, Justin Hsu and Dexter Kozen) "Guarded Kleene Algebra with Tests: Verification of Uninterupted Programs in Nearly Linear Time" has been accepted for publication at POPL 2020.
• Peter O'Hearn's paper "Incorrectness Logic" has been accepted for publication at POPL 2020.
• Fredrik Dahlqvist's paper (with coauthor Dexter Kozen) "Semantics of Higher-Order Probabilistic Programs with Conditioning" has been accepted for publication at POPL 2020.

• This month we welcome many new members to the group! Cristoph Hasse joins the group as an associate professor; Mehrnoosh Sadrzadeh joins the group as an associate professor; Bas Westerbaan joins the group as a research fellow; Sonia Marin joins the group as a research fellow on the ReLiC project; Todd Wayne Schmid joins the group as a PhD student on the ReLiC project; Alex Gheorghiu joins the group as a PhD student on the ReLiC project; Jas Semrl joins the group as a PhD student in UCL's new Foundational AI CDT.
• The PPLV group is proud to announce that Byron Cook has been elected fellow (FREng) of the Royal Society of Engineering: congratulations Byron!
• Paul Brunet's paper "A complete axiomatisation for a fragment of language algebra" has been accepted for publication at CSL 2020.
• Jurriaan Rot's paper (with coauthor Joshua Moerman) "Separation and Renaming in Nominal Sets" has been accepted for publication at CSL 2020.
• Jurriaan Rot's paper (with coauthor Clemens Kupke) "Expressive Logics for Coinductive Predicates" has been accepted for publication at CSL 2020.

• Diana Costa's paper "A four-valued hybrid logic with non-dual modal operators" (with coauthor Manuel A. Martins) has been accepted for publication at DaLi 2019.

• Congratulations to PPLV members Jade Alglave, who has been promoted to Professor of Computer Science, and Fabio Zanasi, who has been promoted to Associate Professor!
• Peter O'Hearn has coauthored an article "Scaling Static Analysis at Facebook" with Dino Distefano, Manuel Fähndrich and Francesco Logozzo for this month's Communications of the ACM. The article gives a high level account of static analysis development and deployment at Facebook (much of it with roots in academic research conducted by PPLV members and affliates past and present), in particular: the feedback loop provided by working closely with engineers, and the methods by which the team overcomes the challenge of scaling up state-of-the-art academic research on program analysis to huge code bases. It can be read at the C.ACM website here.

• The PPLV group hosted MFPS XXXV and CALCO 2019 in the first week of June. Pre-proceedings can be found here.
• Simon Docherty will give a talk titled "Resource Reasoning in Duality-Theoretic Form: Stone-Type Dualities for Bunched and Separation Logics" at TACL 2019 this month.
• Simon Docherty and Reuben Rowe's paper "A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic" has been accepted for publication at TABLEAUX 2019.
• Tobias Kappé, Paul Brunet, Jurriaan Rot, Alexandra Silva, Jana Wagemaker and Fabio Zanasi's paper "Kleene Algebra with Observations" has been accepted for publication at CONCUR 2019.
• Robin Piedeleu and Fabio Zanasi's paper "Bialgebra Semantics for String Diagrams" (with coauthors Filippo Bonchi and Pawel Sobocinski) has been accepted for publication at CONCUR 2019.
• Gerco van Heerdt, Joshua Moerman, Matteo Sammartino and Alexandra Silva's paper "A (Co)algebraic Theory of Succinct Automata" has been published in the Journal of Algebraic and Relational Methods in Computer Science.
• Tiago Ferriera, Matteo Sammartino and Alexandra Silva's paper "Symbolic Register Automata" (with coauthor Loris D'Antoni) has been accepted for publication at CAV 2019.
• Paul Brunet and Alexandra Silva's paper "A Kleene Theorem for Nominal Automata" has been accepted for publication at ICALP 2019.

• Congratulations to Alexandra Silva and Matteo Sammartino on their successful EPSRC grant proposal "Verification of Hardware Concurrency via Model Learning (CLeVer)". More information about the project can be found at the EPSRC site.
• The PPLV group hosts the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) and the 35th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXV) on June 3 - 7 in UCL. Information on registration can be found here.
• Tao Gu and Fabio Zanasi's paper "A Coalgebraic Approach to Probabilistic Logic Programming" has been accepted for publication at CALCO 2019.
• Gerco van Heerdt, Tobias Kappe, Jurriaan Rot, Matteo Sammartino and Alexandra Silva's paper "Tree Automata as Algebras: Minimisation and Determinisation" has been accepted for publication at CALCO 2019.

• David Pym has written an article on bunched logics and resource semantics for the Semantics column of ACM SIGLOG's April newsletter. The article recounts a wealth of logical research undertaken by David and members of the PPLV group, providing the foundations for the program verification formalism Separation Logic, resource-sensitive process calculi and simulation modelling for information security. It can be read here.
• Robin Piedeleu and Fabio Zanasi's paper "Graphical Affine Algebra" (with coauthors Filippo Bonchi and Pawel Sobocinski) has been accepted for publication at this year's LICS. 
• PPLV members Tobias Kappé and Matteo Sammartino are co-organizers (with Remi Eyraud and Guillaume Rabusseau) of a LICS affliated workshop LearnAut 2019, focused on learning, automata theory and grammatical inference. The workshop will be held on June 23rd 2019, and information on registration and submission can be found here.

• Peter O'Hearn is the introductory speaker at Gordon Plotkin's BCS Ada Lovelace lecture on Monday 3rd March. Tickets are available here.
• The first IRIS Day O'Science is to be held on Wednesday 5th March, with contributed talks on topics related to the EPSRC project Interface Reasoning for Interacting Systems. If interested, please contact James Brotherston for more information. 
• David Pym is an invited plenary speaker at the Third Tübingen Conference on Proof-Theoretic Semantics on March 27-30th.
• Alexandra Silva will give a tutorial on verifying networks at the Dagstuhl seminar "Programmable Network Data Planes", to be held 31st March - 5th April. More information can be found here.

• Peter O'Hearn has written a review article on Separation Logic in this month's issue of the Communications of the ACM. It can be read here.
• Tobias Kappé, Paul Brunet, Alexandra Silva and Fabio Zanasi's paper "On series-parallel pomset languages: Rationality, context-freeness and automata" (with coauthor Bas Luttik) has been accepted for publication in the Journal of Algebraic and Logical Methods in Programming.
• Jurriaan Rot joins the group as a Marie Curie Fellow. Welcome Jurriaan!
• Derek Dreyer gives a UCL CS Distinguished Lecture on February 22nd as part of the group's research seminar.
• The PPLV group is advertising the following vacancies: one lecturer, one research fellow (associated with David Pym, Alexandra Silva and Simon Docherty's EPSRC project ReLiC) and many PhD studentships (associated with ReLiC and David Pym, Will Venters, Peter O'Hearn, Edmund Robinson, George Danezis, James Brotherston and Alistair Donaldson's EPSRC project IRIS). 

• Simon Docherty and David Pym's paper "Stone-type Dualities for Separation Logics" has been accepted for publication in the journal Logical Methods in Computer Science.
• Jana Wagemaker joins the group as a PhD student, supervised by Alexandra Silva. Welcome Jana!
• Robin Piedeleu presented the paper "Diagrammatic Algebra: from Linear to Current Systems" at this year's POPL in Lisbon.
• Fabio Zanasi's paper "Causal Inference by String Diagram Surgery" (with coauthors Aleks Kissinger and Bart Jacobs) has been accepted for publication at FoSSaCS 2019.

Older news can be found in the archive.