BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Jeremy Gibbons (University of Oxford)
DTSTART:20240126T110000Z
DTEND:20240126T120000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/1
DESCRIPTION:Title: Turner\, Bird\, Eratosthenes: An Eternal Burning Thread\nby Jerem
y Gibbons (University of Oxford) as part of University of Birmingham theor
etical computer science seminar\n\nLecture held in LG23\, Computer Science
.\n\nAbstract\nThe late David Turner had great taste in language design an
d programming\; the design decisions he made in his languages SASL \, KRC\
, and Miranda over the last 50 years are still influential now. One exampl
e program that he introduced to illustrate lazy evaluation and list compre
hensions in SASL is a one-line recursive “sieve” to generate the infin
ite list of prime numbers.\n\nTurner called this algorithm The Sieve of Er
atosthenes. However\, in a lovely paper “The Genuine Sieve of Eratosthen
es” (JFP\, 2009)\, Melissa O’Neill argued that Turner’s algorithm is
not faithful to Eratosthenes\, and gave a detailed presentation using pri
ority queues of the real thing. She included a variation by Richard Bird\,
that uses only lists but makes clever use of circular programming. Bird d
escribes his circular program again in his textbook “Thinking Functional
ly with Haskell”\, and sets its proof of correctness as an exercise. Unf
ortunately\, his hint for a solution is incorrect. So what should a proof
look like?\n\nOne of the last projects Turner worked on was the notion of
“Total Functional Programming” (eg J.UCS\, 2004)\, “designed to excl
ude the possibility of non-termination”. He observed that most programs
are already structurally recursive or corecursive\, therefore guaranteed t
erminating or productive respectively\, and conjectured that “with more
practice we will find this is always true”. Much as I find this idea app
ealing\, I think we are still some way off\, even after 20 years of “mor
e practice”. I will discuss Bird’s circular Sieve of Eratosthenes as a
challenge problem for Turner’s Total FP.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tomáš Jakl (Czech Academy of Sciences / Czech Technical Universi
ty)
DTSTART:20240202T110000Z
DTEND:20240202T120000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/2
DESCRIPTION:Title: Feferman–Vaught–Mostowski theorems and game comonads\nby Tom
áš Jakl (Czech Academy of Sciences / Czech Technical University) as part
of University of Birmingham theoretical computer science seminar\n\nLectu
re held in LG23\, Computer Science.\n\nAbstract\nIn recent years we have s
een a growing number of examples of model\ncomparison games (such as pebbl
e games or Ehrenfreucht-Fraisse games)\nbeing encoded semantically\, as co
monads on the class of graphs or\nrelational structures. Apart from the co
nnections with logic (via the\nmodel comparison games)\, game comonads can
also express a range of\nimportant parameters in finite model theory and
combinatorics\, such as\ntree-width and tree-depth.\n\nAfter a brief overv
iew of the emerging theory of game comonads\, I\nwill present my joint wor
k with Dan Marsden and Nihil Shah. Our main\nfocus are the so-called Fefer
man–Vaught-Mostowski-type theorems\, which\nexpress when an operation on
models preserves equivalence in a given logic.\n\nProving these theorems
in the comonadic setting amounts to defining\na Kleisli law and checking c
ertain smoothness conditions. Surprisingly\,\nthe main ingredient of our a
pproach is a generalisation of how monoidal\nmonads lift the monoidal stru
cture to the category of algebras.\nFurthermore\, we also show the role of
bilinear maps in this setting and\nhow Johnstone's adjoint lifting theore
m is a special case of all this.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dylan Braithwaite (University of Strathclyde)
DTSTART:20240216T110000Z
DTEND:20240216T120000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/3
DESCRIPTION:Title: Probabilistic Programming with Session Types\nby Dylan Braithwait
e (University of Strathclyde) as part of University of Birmingham theoreti
cal computer science seminar\n\nLecture held in LG23\, Computer Science.\n
\nAbstract\nStatistical inference algorithms often involve an interactive
flow of information. The fundamental principle behind Bayesian statistics
can be seen as an interactive process where a model consists of a likeliho
od function\, which makes a prediction based on some prior knowledge\, and
later receives observations or updates\, as proposed improvements to its
predictions. Similarly\, the idea of interventions in causal inference has
been explained (see Jacobs\, Kissinger and Zanasi) as a kind of factorisa
tion of a Markov kernel into a kernel with additional input and outputs\,
with certain causal relationship encoding the ideal that the inputs occur
after certain outputs.\n\nInteractive protocols of this sort\, with interl
eaved inputs and outputs\, have been modelled in programming languages wit
h session types: type systems for a process calculus which encode encode s
equences of sets annotated with input/output information. Typically semant
ic models of session types make use of an encoding into linear logic\, all
owing process specifications to be interpreted in *-autonomous categories.
Unfortunately\, categories of probabilistic spaces do not usually have su
ch structure\, and so are not suitable for as a full model of linear logic
\, but this structure is far from necessary for modelling simple I/O seque
nces. Recently categorical notions of "combs" have been proposed by severa
l authors as a model for such interactive processes: they provide a genera
l compositional model for processes with sequenced I/O which can be constr
ucted over any monoidal category.\n\nIn this talk I will explain how typic
al operations used in statistical inference algorithms can be succinctly r
epresented as operations on combs\, and outline a description of a simple
language with session types to be interpreted in a (multi)category of comb
s\, and explore how this can be used as a novel form of probabilistic prog
ramming language.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/3/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Kavvos (University of Bristol)
DTSTART:20240223T110000Z
DTEND:20240223T120000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/4
DESCRIPTION:Title: Two-dimensional Kripke Semantics\nby Alex Kavvos (University of B
ristol) as part of University of Birmingham theoretical computer science s
eminar\n\nLecture held in G33\, Aston Webb.\n\nAbstract\nThe study of moda
l logic has witnessed tremendous development following the introduction of
Kripke semantics. However\, recent developments in programming languages
and type theory have led to a second way of studying modalities\, namely t
hrough their categorical semantics. We show how the two correspond.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nesta van der Schaaf (University of Edinburgh)
DTSTART:20240301T110000Z
DTEND:20240301T120000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/5
DESCRIPTION:Title: Ordered Locales\nby Nesta van der Schaaf (University of Edinburgh
) as part of University of Birmingham theoretical computer science seminar
\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nOrder and topolo
gy both abound in mathematics\, often even together. Combined\, they form
the notion of an ordered topological space. How can this notion be suitabl
y generalised to the theory of point-free topology? In this talk we will d
iscuss one possibility\, based on the so-called Egli-Milner relation. To k
eep the talk accessible\, we start with an introduction to the definition
of locales and describe their adjunction with topological spaces. After th
at\, we show how this adjunction can be extended to certain categories of
ordered spaces and the newly introduced ordered locales. To finish the tal
k we highlight some ongoing work. First\, we describe how we are using the
se techniques to study aspects of relativity theory. In particular\, we de
scribe ingredients for a "causal boundary" construction\, and show how "do
mains of dependence" can be recovered as a natural Grothendieck topology o
n ordered locales. Lastly\, time permitting\, we discuss an "internal" gen
eralisation of ordered locales. (Based on joint work with Chris Heunen and
Prakash Panangaden.)\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Charles Grellois (University of Sheffield)
DTSTART:20240308T110000Z
DTEND:20240308T120000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/6
DESCRIPTION:Title: Semantic approaches to verification of functional programs\nby Ch
arles Grellois (University of Sheffield) as part of University of Birmingh
am theoretical computer science seminar\n\nLecture held in LG23\, Computer
Science.\n\nAbstract\nWhat can the semantics of a program bring when it c
omes to verification? Almost a decade ago\, during my PhD under the superv
ision of Paul-André Melliès\, we showed that the main problem considered
in higher-order model-checking could be actually reduced to computing the
semantics of the program in some models of linear logic\, enriched with a
modality and a tricky inductive-coinductive fixpoint operator. Decidabili
ty would follow from the existence of finitary models in which this "seman
tic verification procedure" is possible.\n\nAn interesting point in this a
pproach is that this "practical" problem from verification leads us to act
ually consider new and very relevant extensions of the semantics of linear
logic\, notably since the higher-order model-checking problem requires mi
xing inductive and coinductive reasoning\; but the interplay of programs a
nd alternating tree automata is also surprisingly natural at the light of
linear logic.\n\nThe "original" higher-order model-checking problem was pr
oved decidable by Ong in 2006\; it led to many alternative proofs\, explor
ing a vast area of theoretical computer science. I believe that this explo
ration is far from over\, and will discuss new potential directions involv
ing cyclic proofs\, infinitary reasoning\, extensional collapses...\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leo Lobski (University College London)
DTSTART:20240315T110000Z
DTEND:20240315T120000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/7
DESCRIPTION:Title: Towards functorial chemistry: completeness and universality for react
ion representation\nby Leo Lobski (University College London) as part
of University of Birmingham theoretical computer science seminar\n\nLectur
e held in LG23\, Computer Science.\n\nAbstract\nOrganic molecules can be r
epresented mathematically using labelled graphs [1]. Recently\, the graph
approach to chemistry has been extended to reactions using the techniques
of graph rewriting [2\,3]. While representing reactions lies at the heart
of mathematical chemistry\, the focus to date has been on the "forward" di
rection of reaction prediction and composition. The "reverse" direction of
discovering reaction pathways to new compounds is\, however\, one of the
main aims of modern chemical engineering. The methodology of this field\,
known as retrosynthetic analysis\, is well-established and widely practise
d [4\,5\,6\,7]\, but has received significantly less mathematical attentio
n.\n\nIn this talk\, I will suggest taking the basic units of retrosynthet
ic analysis - disconnection rules - as first-class citizens of reaction re
presentation. The mathematical and conceptual justification for doing so l
ies in the fact that both disconnection rules and formalised reactions can
be arranged into monoidal categories [8]\, such that there is a monoidal
functor taking each (composable) sequence of disconnection rules to a reac
tion. Our main result shows that\, under a certain axiomatisation of the d
isconnection rules\, the functor is faithful and an opfibration. This impl
ies that every reaction can be decomposed into a sequence of disconnection
rules (universality) in an essentially unique way (completeness).\n\n[1]
D. Bonchev and D.H. Rouvray (eds). Chemical Graph Theory: Introduction and
Fundamentals. Abacus Press / Gordon & Breach Science Publishers. 1991.\n\
n[2] J.L. Andersen\, C. Flamm\, D. Merkle\, and P.F. Stadler. Inferring ch
emical reaction patterns using rule composition in graph grammars. J. Syst
. Chem. 2013.\n\n[3] J.L. Andersen\, C. Flamm\, D. Merkle\, and P.F. Stadl
er. An intermediate level of abstraction for computational systems chemist
ry. Philos. Trans. R. Soc. 2017.\n\n[4] E.J. Corey and X. Cheng. The logic
of chemical synthesis. John Wiley. 1989.\n\n[5] S. Warren and P. Wyatt. O
rganic synthesis: the disconnection approach. Wiley. 2008.\n\n[6] J. Clayd
en\, N. Greeves\, and S. Warren. Organic chemistry. OUP. 2012.\n\n[7] Y. S
un and N.V. Sahinidis. Computer-aided retrosynthetic design: fundamentals\
, tools\, and outlook. Curr. Opin. Chem. Eng. 2022.\n\n[8] E. Gale\, L. Lo
bski\, and F. Zanasi. A Categorical Approach to Synthetic Chemistry. Theor
etical Aspects of Computing - ICTAC. 2023.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Cristina Matache (University of Edinburgh)
DTSTART:20240322T110000Z
DTEND:20240322T120000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/8
DESCRIPTION:Title: Parameterized algebraic theories and applications\nby Cristina Ma
tache (University of Edinburgh) as part of University of Birmingham theore
tical computer science seminar\n\nLecture held in LG23\, Computer Science.
\n\nAbstract\nThe framework of algebraic theories has proved useful for re
asoning equationally about impure computation\, such as state\, nondetermi
nism\, probabilistic choice. In this talk\, I will review parameterized al
gebraic theories\, an extension of algebraic theories that allows for bind
ing. I will show how parameterized theories can be used to give an equatio
nal account of scoped effects\, a class of effects that does not fit into
the plain algebraic framework. Finally\, I will sketch work in progress ab
out axiomatizing dynamic creation of threads using parameterized theories.
\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/8/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Pablo Donato (École Polytechnique)
DTSTART:20240419T100000Z
DTEND:20240419T110000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/9
DESCRIPTION:Title: Deep Inference for Graphical Theorem Proving\nby Pablo Donato (É
cole Polytechnique) as part of University of Birmingham theoretical comput
er science seminar\n\nLecture held in TBA.\n\nAbstract\nIn this talk\, I w
ill summarize my four-year thesis journey focused on designing graphical u
ser interfaces (GUIs) for interactive proof construction. Deep inference p
roof theory guided my approach\, inspiring innovative representations and
interactions with logical entities.\n\nThe first part of the talk will int
roduce the Proof-by-Action paradigm\, enabling users to construct proofs t
hrough direct manipulation of the proof state. Actema\, a GUI prototype fo
r intuitionistic first-order logic\, demonstrates this approach with its d
rag-and-drop proof tactic grounded in "subformula linking"\, a recent tech
nique based on the calculus of structures.\n\nIn the subsequent discussion
\, I will present an open-ended line of research where I aim to get rid of
traditional symbolic formulas\, in favor of more structured and iconic re
presentations of the proof state. This includes the development of so-call
ed "bubble calculi"\, a family of systems that reframe and extend the theo
ry of nested sequents as local rewriting systems. Bubble calculi enjoy a g
raphical and topological interpretation\, enable efficient sharing of cont
exts among subgoals\, and capture both intuitionistic\, dual-intuitionisti
c\, bi-intuitionistic and classical logic in a unified way.\n\nFinally\, I
will introduce the flower calculus\, an intuitionistic refinement of C.S.
Peirce's theory of existential graphs\, understood as a system for intera
ctive proof building. It provides more iconic and economical means of reas
oning than bubble calculi\, by exposing a small number of expressive rules
that apply to the goals themselves\, removing completely the need for log
ical connectives. I will conclude with a demonstration of the Flower Prove
r\, another prototype of GUI in the Proof-by-Action paradigm\, whose actio
ns map directly to the rules of the flower calculus.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Satoshi Kura (National Institute of Informatics / University of Ox
ford)
DTSTART:20240209T110000Z
DTEND:20240209T120000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/10
DESCRIPTION:Title: Higher-Order Weakest Precondition Transformers via a CPS Transformat
ion\nby Satoshi Kura (National Institute of Informatics / University o
f Oxford) as part of University of Birmingham theoretical computer science
seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nWeakest
preconditions are essential notions for program verification. There are ma
ny variations of weakest preconditions\, and their uniform treatment has b
een studied using category-theoretic notions like monads. In this talk\, w
e consider weakest preconditions for a higher-order functional language wi
th computational effects and recursion and show that we can syntactically
compute them via a CPS transformation. We prove our main theorem in a gene
ral setting\, which enables us to instantiate our result to several proble
ms of program verification. Our result generalises two existing works on p
rogram verification: (1) trace properties and may-/must-reachability studi
ed by Kobayashi et al. and (2) expected cost analyses studied by Avanzini
et al. We also obtain a new instance of cost moment analyses using our mai
n theorem.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Igor Carboni Oliveira (University of Warwick)
DTSTART:20240318T130000Z
DTEND:20240318T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/11
DESCRIPTION:Title: Polynomial-Time Pseudodeterministic Construction of Primes\nby I
gor Carboni Oliveira (University of Warwick) as part of University of Birm
ingham theoretical computer science seminar\n\nLecture held in LG23\, Comp
uter Science.\n\nAbstract\nA randomized algorithm for a search problem is
pseudodeterministic if it produces a fixed canonical solution to the searc
h problem with high probability. In their seminal work on the topic\, Gat
and Goldwasser posed as their main open problem whether prime numbers can
be pseudodeterministically constructed in polynomial time.\n\nWe provide a
positive solution to this question in the infinitely-often regime. In mor
e detail\, we give an unconditional polynomial-time randomized algorithm $
B$ such that\, for infinitely many values of $n$\, $B(1^n)$ outputs a cano
nical $n$-bit prime $p_n$ with high probability. More generally\, we prove
that for every dense property $Q$ of strings that can be decided in polyn
omial time\, there is an infinitely-often pseudodeterministic polynomial-t
ime construction of strings satisfying $Q$. This improves upon a subexpone
ntial-time construction of Oliveira and Santhanam.\n\nOur construction use
s several new ideas\, including a novel bootstrapping technique for pseudo
deterministic constructions\, and a quantitative optimization of the unifo
rm hardness-randomness framework of Chen and\nTell\, using a variant of th
e Shaltiel-Umans generator.\n\nReference: https://eccc.weizmann.ac.il/repo
rt/2023/076/\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hugo Ferée (IRIF)
DTSTART:20240418T100000Z
DTEND:20240418T110000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/12
DESCRIPTION:Title: Mechanised uniform interpolation for modal logics K\, GL and iSL
\nby Hugo Ferée (IRIF) as part of University of Birmingham theoretical co
mputer science seminar\n\nLecture held in Old Gym LG06.\n\nAbstract\nThe u
niform interpolation property in a given logic can be understood as the de
finability of propositional quantifiers. We will describe here proof-theor
etic proof of this property for three modal logics: iSL (for which this is
a new result)\, K and GL (for which we fixed an issue in the existing pro
of). All three proofs are implemented in the Coq proof assistant\, making
the computation of the interpolants effective.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrew Sogokon (Lancaster University)
DTSTART:20240510T100000Z
DTEND:20240510T110000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/14
DESCRIPTION:Title: Inductive Invariants in Continuous Systems\nby Andrew Sogokon (L
ancaster University) as part of University of Birmingham theoretical compu
ter science seminar\n\nLecture held in Aston Webb\, WG12.\n\nAbstract\nThe
problem of checking whether a set is an inductive invariant is of fundame
ntal importance to formal safety verification. While the tools required fo
r this problem in the typical discrete setting are rather straightforward
and quite standard in computer science\, the situation is markedly differe
nt in continuous systems (i.e. systems where time does not advance in disc
rete time steps\, but instead passes continuously\, e.g. as in systems def
ined by ordinary differential equations). This problem was considered by m
athematicians since the 1940s\, who developed several characterizations wh
ich\, unfortunately\, do not provide an effective way of checking whether
a given set is an inductive invariant for a given continuous system. In th
e past decade great progress has been made by computer scientists in devel
oping the tools for reasoning about continuous systems and powerful result
s have been reported which essentially solve the problem of inductive inva
riant checking algorithmically under some reasonable restrictions on the n
ature of the set and the kind of continuous system. In this talk\, I will
present an overview of some of the progress that has been made and will ou
tline some fundamental practical limitations inherent in current approache
s.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Calum Hughes (University of Manchester)
DTSTART:20240517T100000Z
DTEND:20240517T110000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/15
DESCRIPTION:Title: Models of Martin-Löf Type Theory and Algebraic Model Structures
\nby Calum Hughes (University of Manchester) as part of University of Birm
ingham theoretical computer science seminar\n\nLecture held in Aston Webb\
, WG12.\n\nAbstract\nKnown models of Martin-Löf Type Theory (MLTT) includ
e isofibrations in the category of groupoids and Kan fibrations in the cat
egory of simplicial sets. It is an open problem to prove constructively th
at Kan fibrations model Homotopy Type Theory. One suggested way to approac
h this problem is with an algebraic perspective\; the idea being that by k
eeping track of the algebraic data throughout calculations\, proofs become
more constructive. Classically\, normal isofibrations are the algebras fo
r the right class of a type theoretic algebraic weak factorisation system
which form part of an algebraic model structure. Constructively\, however\
, this link breaks down as this algebraic model structure fails to exist.\
n\nIn this talk\, I will show how we can re-establish this connection by p
roving constructively that cloven isofibrations are the algebras for the r
ight class of a type theoretic algebraic weak factorisation system which f
orm part of an algebraic model structure. I will also briefly discuss how
this result holds more generally\, providing an internal-groupoidal model
of MLTT with links to an algebraic model structure.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sam van Gool (IRIF\, Paris)
DTSTART:20240524T100000Z
DTEND:20240524T110000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/16
DESCRIPTION:Title: Deciding unifiability by folding coalgebras\nby Sam van Gool (IR
IF\, Paris) as part of University of Birmingham theoretical computer scien
ce seminar\n\nLecture held in Aston Webb\, WG12.\n\nAbstract\nThe unifiabi
lity problem for a logic L asks to decide whether or not\nthere exists a s
yntactic substitution that renders two given formulas\nequivalent in L.\n\
nThe first objective of this talk is to show how the unifiability problem\
nfor a logic can often be usefully reformulated as a problem about\nhomomo
rphisms between coalgebras.\n\nThe second objective is to showcase this me
thod in the context of the\ntemporal logic of next\, that is\, classical p
ropositional logic with a\ndeterministic unary modality. In this specific
case\, we show that the\nunifiability problem is equivalent to a homomorph
ism mapping problem for\na sequence of graphs known in the literature as D
e Bruijn graphs. We\nsolve the homomorphism mapping problem\, employing me
thods rooted in\nstring compression\, and thus establishing decidability o
f unifiability\nfor the temporal logic of next.\n\nThis work is part of an
ongoing collaboration with Johannes Marti and\nMichelle Sweering.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/16/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ambroise Lafont (École Polytechnique)
DTSTART:20240531T100000Z
DTEND:20240531T110000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/17
DESCRIPTION:Title: A diagram editor to mechanise categorical proofs\nby Ambroise La
font (École Polytechnique) as part of University of Birmingham theoretica
l computer science seminar\n\nLecture held in LG23\, Computer Science.\n\n
Abstract\nDiagrammatic proofs are ubiquitous in certain areas of mathemati
cs\, especially in category theory. Mechanising such proofs is a tedious t
ask because proof assistants (such as Coq) are text based. We present a pr
ototypical diagram editor to make this process easier\, building upon the
vscode extension coq-lsp for the Coq proof assistant and a web application
(https://amblafont.github.io/graph-editor/index.html).\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Paul Taylor (University of Birmingham)
DTSTART:20240426T100000Z
DTEND:20240426T110000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/18
DESCRIPTION:Title: Free algebras for functors\, with not an ordinal in sight\nby Pa
ul Taylor (University of Birmingham) as part of University of Birmingham t
heoretical computer science seminar\n\nLecture held in Old Gym\, LG10.\n\n
Abstract\nMartin Escardo challenged me to make Pataraia's fixed point\nthe
orem "predicative". Whilst I have never understood the\nmotivation for th
at notion\, I have eliminated one instance\nof impredicativity and isolate
d the infinitary aspects to\na single specific directed join.\n\nSo then I
looked for the categorical version. Pataraia's\nidea plays a quite small
part: the construction uses ideas\nfrom categorical algebra since its orig
ins\, and if I were\nto credit one person it would be Joachim Lambek.\n\nT
he problem breaks into two parts\, one finitary and the\nother infinitary.
The infinitary part says that the\ncategory of pointed endofunctors of a
small category\nwith coequalisers is filtered\, so has a terminal object\
nif the given category has the required filtered colimit.\nThis is probabl
y widely applicable as an alternative to\ntransfinite methods.\n\nThe fini
tary construction is that of fragments of the\ninitial algebra. It may be
done in several ways\, but\none is to consider coalgebras for the given f
unctor\nthat are have a cone over all algebras for it. We\nidentify a "sp
ecial condition" that this construction\nsatisfies and that ensures that t
he terminal endofunctor\n(applied to any object) yields the terminal objec
t of\nthe finitary category\, which is the required initial\nalgebra of th
e functor.\n\nThe hope is that a similar finitary category of\npartial mod
els could be found for more complex\nsystems of algebra and logic and that
these would\ncorrespond to the intermediate stages in proof\ntheoretic ar
guments for normalisation\, cut\nelimination etc.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Wilmer Ricciotti (University of Edinburgh)
DTSTART:20240607T100000Z
DTEND:20240607T110000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/19
DESCRIPTION:Title: Syntactic representation of program execution history\nby Wilmer
Ricciotti (University of Edinburgh) as part of University of Birmingham t
heoretical computer science seminar\n\nLecture held in LG23\, Computer Sci
ence.\n\nAbstract\nAuditing is an increasingly important operation for com
puter programming\, for example in security (e.g. to enable history-based
access control) and to enable reproducibility and accountability (e.g. pro
venance in scientific programming). Engineering a software system to allow
history-based auditing by means of ad-hoc instrumentation requires a subs
tantial effort: the development of general-purpose infrastructure is thus
very important to achieve the goal of making such techniques widely availa
ble.\n\nInspired by work on Justification Logic\, we study the syntactic r
epresentation of program execution history in the setting of the Calculus
of Audited Units\, a core functional language providing auditing as a firs
t-class operation. CAU automatically materializes execution history as a d
ata structure and can be implemented by a call-by-value abstract machine i
n a relatively efficient way. To prove the correctness of our machine\, we
extend the language with explicit substitutions and explicit auditing ope
rations.\n\nWe discuss applications of auditing by showing how to use it t
o derive various provenance views relating program output to its input. Fi
nally\, we present some current work showing a connection between the synt
actic representation of execution history and the standardisation theorem
for the lambda calculus.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Stepan Kuznetsov (Steklov Mathematical Insititute)
DTSTART:20240919T100000Z
DTEND:20240919T110000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/21
DESCRIPTION:Title: Substructural logics with Kleene star\nby Stepan Kuznetsov (Stek
lov Mathematical Insititute) as part of University of Birmingham theoretic
al computer science seminar\n\nLecture held in Murray UG07.\n\nAbstract\nS
ubstructural logics are logics given by sequent calculi which lack all or
some of the structural rules: contraction\, permutation\, weakening. Such
logics may be extended by an intriguing operation called Kleene star. The
basic logic here is so-called action logic\, which extends the multiplica
tive-additive Lambek calculus. There are two ways of axiomatising the Klee
ne star: a fixpoint one\, yielding action logic\, and a stronger one using
the omega-rule\, which gives infinitary action logic.\n \nAction logic an
d infinitary action logic\, both being undecidable\, have different algori
thmic complexity properties. Action logic is finitely axiomatisable\, thus
\, for this logic undecidability means $\\Sigma^0_1$-completeness. In cont
rast\, infinitary action logic and its extensions (by finite sets of extra
axioms and by so-called subexponential modalities) feature a range of int
eresting complexity level\, from $\\Pi^0_1$ to $\\Pi^1_1$\, with hyperarit
hmetical classes in between.\n \nIn the talk\, we shall give a survey of a
lgorithmic and semantical results for action logic and its variants. These
results include well-known ones by V. Pratt\, D. Kozen\, W. Buszkowski\,
E. Palka\, and others\, as well as recent results obtained by the author\,
solely and in co-authorship with S. Speranski and T. Pshenitsyn.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/21/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Arkadev Chattopadhyay (Tata Institute of Fundamental Research)
DTSTART:20240927T130000Z
DTEND:20240927T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/22
DESCRIPTION:Title: The Power of Randomness in Query and Communication\nby Arkadev C
hattopadhyay (Tata Institute of Fundamental Research) as part of Universit
y of Birmingham theoretical computer science seminar\n\nLecture held in LG
23\, Computer Science.\n\nAbstract\nHow powerful is randomness for speedin
g up algorithms? This is a central question in theoretical computer scienc
e. But answering it in the Turing machine model seems pretty out of reach
for now. We turn the spotlight on two simple and very well studied models
of computing: query and 2-party communication. These models are closely re
lated. In this talk\, I will give a (biased) survey of some of the intrigu
ing questions that these models raise about the basic nature of randomness
.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/22/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Christian Konrad (University of Bristol)
DTSTART:20241004T130000Z
DTEND:20241004T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/23
DESCRIPTION:Title: Maximal Matching in Bounded-deletion Streams\nby Christian Konra
d (University of Bristol) as part of University of Birmingham theoretical
computer science seminar\n\nLecture held in LG23\, Computer Science.\n\nAb
stract\nWe study the Maximal Matching problem in bounded-deletion graph st
reams. In this setting\, a graph $G$ is revealed as an arbitrary sequence
of edge insertions and deletions\, where the number of insertions is unres
tricted but the number of deletions is guaranteed to be at most $K$\, for
some given parameter $K$. The single-pass streaming space complexity of th
is problem is known to be $\\Theta(n^2)$ when $K$ is unrestricted\, where
$n$ is the number of vertices of the input graph. We present a new algorit
hm and a matching lower bound result that together give a tight understand
ing (up to poly-log factors) of how the space complexity of Maximal Matchi
ng evolves as a function of the parameter $K$.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/23/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Daniel Gratzer (Aarhus University)
DTSTART:20241018T130000Z
DTEND:20241018T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/24
DESCRIPTION:Title: On synthetic category theory in homotopy type theory\nby Daniel
Gratzer (Aarhus University) as part of University of Birmingham theoretica
l computer science seminar\n\nLecture held in LG23\, Computer Science.\n\n
Abstract\nRiehl--Shulman 2017 introduced a version of homotopy type theory
(simplicial type theory or STT) which replaces homotopy type theory's slo
gan that "types are spaces" with the somewhat wordier "some types are (∞
\,1)-categories". Remarkably\, working in homotopy type theory means that
we are able to largely ignore the ∞- part of this slogan\, resulting in
simple proofs of difficult classical results. In this talk we give an intr
oduction to STT (presupposing only knowledge of type theory and a little e
xposure to ordinary categories) and discuss recent work by Gratzer\, Weinb
erger\, and Buchholtz on the topic. In particular\, we will focus on the c
onstruction of a particular type within STT which corresponds to the (infi
nity categorical version of) the category of sets. We shall see that this
type can be characterized as a *directed* univalent universe and go throug
h the first consequences of its addition to STT.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/24/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Giovanni Soldà (Ghent University)
DTSTART:20241108T140000Z
DTEND:20241108T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/25
DESCRIPTION:Title: A proof of Nash-Williams theorem in ATR0\nby Giovanni Soldà (Gh
ent University) as part of University of Birmingham theoretical computer s
cience seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nIn
[1]\, Crispin Nash-Williams proved that if (Q\, ≤Q) is a well quasi-ord
er (henceforth wqo)\, then so is the set of transfinite sequences over Q w
ith finite range\, ordered by embeddability. In this talk\, we will show t
hat this result is provable in the subsystem of second-order arithmetic AT
R0: together with previous results by Shore [2]\, this determines the reve
rse mathematical strength of Nash-Williams’ result. In order to do this\
, we will go via the notion of better quasi-order\, which makes it possibl
e to develop an equivalence between the iterated powerset of a qo Q and th
e iterated powerset over Q. This is joint work with Fedor Pakhomov.\n\nRef
erences\n\n[1] C. Nash-Williams\, On well-quasi-ordering transfinite seque
nces\, Mathematical Proceedings of the Cambridge Philosophical Society 61
(1965)\, no. 1\, 33–39.\n[2] R. A. Shore\, On the strength of Fraïssé
’s conjecture\, Logical methods: In honor of Anil Nerode’s sixtieth bi
rthday\, 1993\, pp. 782–813.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/25/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Luca Reggio (Università degli Studi di Milano)
DTSTART:20241122T140000Z
DTEND:20241122T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/26
DESCRIPTION:Title: Resource-bounded logics: a categorical and modal view\nby Luca R
eggio (Università degli Studi di Milano) as part of University of Birming
ham theoretical computer science seminar\n\nLecture held in LG23\, Compute
r Science.\n\nAbstract\nLogics obtained by constraining the available synt
actic resources\, such as first-order logic with a finite number of variab
les or with bounded quantifier rank\, are central to finite model theory a
nd descriptive complexity. I will describe a categorical approach to the s
tudy of these logic fragments based on so-called game comonads. I will exp
lain how the main properties of the categories of coalgebras for these com
onads lead to the axiomatic notion of arboreal categories\, which in turn
suggests a modal treatment of many resource-bounded logics.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/26/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sebastian Enqvist (Stockholm University)
DTSTART:20241129T140000Z
DTEND:20241129T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/27
DESCRIPTION:Title: Computational content of classical cyclic proofs\nby Sebastian E
nqvist (Stockholm University) as part of University of Birmingham theoreti
cal computer science seminar\n\nLecture held in LG23\, Computer Science.\n
\nAbstract\nMuch of the literature on cyclic and non-wellfounded proofs vi
ew such proofs from a Curry-Howard or "proofs-as-programs" perspective. Cy
clic proofs are natural in this regard as they handle induction by allowin
g proofs themselves to be recursively defined\, rather than adding extra i
nduction axioms or rules. In this talk I will present some early-stage wor
k on combining this approach with a long-standing theme in proof theory\,
the computational content of classical proofs. I will begin by giving some
background and general thoughts on computational interpretations of class
ical logic. After that I will present a proposal for an approach\, based o
n a version of Parigot's lambda-mu-calculus with non-wellfounded terms. I
will sketch how this calculus can be used to extract computational content
from proofs in classical FOL extended with inductive predicates. I will a
lso talk about ongoing work to establish some basic properties of the calc
ulus\, in particular subject reduction\, confluence and normalization.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/27/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tamio-Vesa Nakajima (University of Oxford)
DTSTART:20241011T130000Z
DTEND:20241011T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/28
DESCRIPTION:Title: Bipartite versus triangle-free subgraphs\nby Tamio-Vesa Nakajima
(University of Oxford) as part of University of Birmingham theoretical co
mputer science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbst
ract\nSuppose we are given a graph G\, which we are promised has a biparti
te subgraph admitting x edges. Can we then find a triangle-free subgraph a
dmitting a * x edges\, for some approximation ratio a? This talk will disc
uss the complexity of this problem for various values of a\, as well as go
through connections with other computational problem such as maximum cut\
, and maximisation versions of PCSPs. As an application\, we will discuss
a maximisation version of the Brakensiek-Guruswami conjecture for the appr
oximate graph homomorphism problem.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/28/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sky Wilshaw (University of Nottingham)
DTSTART:20241025T130000Z
DTEND:20241025T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/29
DESCRIPTION:Title: New Foundations: the story of a large formalisation project\nby
Sky Wilshaw (University of Nottingham) as part of University of Birmingham
theoretical computer science seminar\n\nLecture held in LG23\, Computer S
cience.\n\nAbstract\nIn this talk\, I will discuss the experiences and cha
llenges of running a successful formalisation project: proving the consist
ency of Quine’s set theory New Foundations. The main focus will be on th
e interesting and unexpected ways in which large formalisation projects di
ffer from small ones\, and how we can use formalisation to get better at
‘paper’ mathematics.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/29/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Soumyajit Paul (University of Liverpool)
DTSTART:20241101T140000Z
DTEND:20241101T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/30
DESCRIPTION:Title: Drinking is not good for driving\, nor for computation : complexity
of solving games with imperfect information\nby Soumyajit Paul (Univer
sity of Liverpool) as part of University of Birmingham theoretical compute
r science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\
nIn perfect information games such as Chess and Go\, players observe every
thing. Zermelo\, in his seminal work\, showed that the winner in a win-los
e version of Chess can be determined using backward induction. This provid
ed a polynomial time algorithm for computing the winner in any perfect inf
ormation game. On the other hand\, in games with imperfect information suc
h as Bridge and Poker\, players don't observe opponents' hands of cards an
d hence have partial knowledge while playing. Imperfect information makes
the task of computing optimal strategies difficult: the problem is NP-hard
in general. There are tractable subclasses\, such as when players have pe
rfect recall\, i.e. players perfectly remember their past decisions. These
games can be solved in polynomial time. Imperfect recall in general can c
apture strange situations. Players can even forget if they have encountere
d the same decision point before\, demonstrated using the game of absentmi
nded driver by Piccione and Rubinstein.\n\nIn this talk\, we will take a t
our of the complexity of solving finite games with imperfect information.
We will discuss existing results and also new complexity bounds for solvin
g imperfect recall games. For new lower bounds\, we relate to problems suc
h as the Square Root Sum problem as well as complexity classes involving c
omputation over reals. More precisely\, we consider the Existential Theor
y of Reals (ETR) and other fragments of the First Order Theory of Reals (F
OTR). We will also see new tractable classes within imperfect recall. This
is from joint work with Hugo Gimbert\, B. Srivathsan and Kristoffer Arnsf
elt Hansen.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/30/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sergey Goncharov (University of Birmingham)
DTSTART:20241115T140000Z
DTEND:20241115T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/31
DESCRIPTION:Title: Introduction to Higher-Order Mathematical Operational Semantics\
nby Sergey Goncharov (University of Birmingham) as part of University of B
irmingham theoretical computer science seminar\n\nLecture held in LG23\, C
omputer Science.\n\nAbstract\nReasoning about program equivalence in highe
r-order setting is one of the central topics in computer science\, with th
e classical lambda-calculus as a prototypical example and with its countle
ss flavors and extensions thereof\, all the way up to Haskell and OCaml. A
recently emerged program of higher-order mathematical operational semanti
cs aims to abstract and unify reasoning methods for such languages on the
basis of two parameters: the language syntax and its (small-step) operatio
nal semantics. Thus\, higher-order mathematical operational semantics is a
natural extension of the pioneering Turi and Plotkin's (first-order) math
ematical operational semantics. Our program takes its origin from a joint
POPL-2023 publication with Stelios Tsampas\, Henning Urbat\, Stefan Milius
\, and Lutz Schröder\, on which my present talk is largely based. Additio
nally\, I will survey\, more succinctly\, subsequent advances of this prog
ram\, outline challenges and perspectives for further work.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/31/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Amin Karamlou (Oxford)
DTSTART:20241206T140000Z
DTEND:20241206T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/32
DESCRIPTION:Title: Quantum relaxations of CSP and structure isomorphism\nby Amin Ka
ramlou (Oxford) as part of University of Birmingham theoretical computer s
cience seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nWe
investigate quantum relaxations of two key decision problems in computer
science: the constraint satisfaction problem (CSP) and the structure isomo
rphism problem. CSP asks whether a homomorphism exists between two relatio
nal structures\, while structure isomorphism seeks an isomorphism between
them. In recent years\, it has become increasingly apparent that many spec
ial cases of CSP can be reformulated in terms of the existence of perfect
classical strategies in non-local games\, a key topic of study in quantum
information theory. These games have allowed us to study quantum advantage
in relation to many important decision problems\, such as the k-colouring
problem\, and the problem of solving binary constraint systems. Abramsky
et al. (2017) have shown that all of these games can be seen as special in
stances of a non-local CSP game. Moreover\, they show that perfect quantum
strategies in this CSP game can be viewed as Kleisli morphisms of a grade
d monad on the category of relational structures\, which they dub the quan
tum monad. In this way\, the quantum monad provides a categorical characte
risation of quantum advantage for the non-local CSP game.\n\nIn this talk
we shall answer several open questions about the non-local CSP game. We th
en study a non-local structure isomorphism game\, which generalises the we
ll-studied graph isomorphism game. We show how the construction of the qua
ntum monad can be refined to provide categorical semantics for quantum str
ategies in this game. This results in a category where morphisms coincide
with quantum homomorphisms and isomorphisms coincide with quantum isomorph
isms.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/32/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Morgan Rogers (LIPN\, Université Paris 13)
DTSTART:20241213T140000Z
DTEND:20241213T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/33
DESCRIPTION:Title: Topoi with enough points\nby Morgan Rogers (LIPN\, Université P
aris 13) as part of University of Birmingham theoretical computer science
seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\njww Ivan
Di Liberti\, https://arxiv.org/pdf/2403.15338\n\nTo include a wider audien
ce\, here are two perspectives on the topic of my talk.\n\nGrothendieck to
poses are sometimes described as generalized spaces\, owing to the fact th
at a motivating example is the category of sheaves on a topological space
and many properties of the space are reflected in the categorical structur
e in a way that can be generalized to other Grothendieck toposes. For suff
iciently separated spaces (the so-called sober spaces\, notably including
all Hausdorff spaces)\, the construction of the category of sheaves is eve
n a fully faithful embedding of spaces and continuous maps into the (2-)ca
tegory of toposes and geometric morphisms\, and points become geometric mo
rphisms Set --> Sh(X). One consequence of this point of view is that one m
ight expect to be able to apply pointwise reasoning to toposes\, to unders
tand the objects and constructs within a topos by examining what they look
like at points. This turns out not to be possible in general! A topos is
said to have enough points if any pair of distinct morphisms is distinguis
hed by a point.\n\nGrothendieck toposes classify theories in geometric log
ic\, a fragment of infinitary first-order logic in which only finite conju
nctions\, set-indexed disjunctions and existential quantification are allo
wed in the construction of formulae (and axioms are sequents asserting tha
t one such formula entails another). That a topos E "classifies" such a th
eory T means that the models of T in any Grothendieck topos F correspond t
o geometric morphisms F --> E. In particular\, set-theoretic models corres
pond to morphisms Set --> E\, which is to say points of E. The classifying
topos of T having enough points exactly says that T is complete with resp
ect to its set-valued models.\n\nSome sufficient conditions for a topos to
have enough points emerged fairly early in the development of topos theor
y (Deligne\, Makkai-Reyes)\, but the extent to which they are related to o
ne another or could be extended was not apparent. In this talk I present t
he state of the art\, alongside some examples indicating that improving ou
r results will be tricky!\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/33/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Laura Bocchi (University of Kent)
DTSTART:20250124T140000Z
DTEND:20250124T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/34
DESCRIPTION:Title: Asynchronous Session Subtyping by Trace Relaxation\nby Laura B
occhi (University of Kent) as part of University of Birmingham theoretical
computer science seminar\n\nLecture held in LG23\, Computer Science.\n\nA
bstract\nSession types are a formalism for modelling structured communicat
ions in concurrent systems and can be seamlessly implemented into programm
ing languages. Session subtyping answers the question of whether a program
in a concurrent system can be safely substituted for another\, when their
communication behaviours are described by session types. \nAsynchronous s
ession subtyping is undecidable in general\, hence the interest in devisin
g sound (though incomplete) subtyping algorithms. State-of-the-art methods
rely on a data structure known as input trees. I will present an alternat
ive approach that replaces input trees with sets of traces\, enabling the
application of abstract interpretation techniques to this problem. This tr
ace-based approach introduces a novel way to relax (enlarge) trace sets wh
ile maintaining observable subtyping properties. Crucially\, these relaxat
ions can be finitely represented\, even when the corresponding input trees
are arbitrarily large. This method can be instantiated using regular expr
essions\, enabling us to mechanically prove subtyping for communication pa
tterns previously beyond reach.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/34/
END:VEVENT
BEGIN:VEVENT
SUMMARY:John Sylvester (University of Liverpool)
DTSTART:20250131T140000Z
DTEND:20250131T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/35
DESCRIPTION:Title: Adjacency Labeling Schemes for Small Classes\nby John Sylvester
(University of Liverpool) as part of University of Birmingham theoretical
computer science seminar\n\nLecture held in LG23\, Computer Science.\n\nAb
stract\nAn adjacency labeling scheme for a class of graphs $\\mathcal{C}$
defines\, for any $n$-vertex $G \\in \\mathcal{C}$\, an assignment of labe
ls to each vertex in $G$ so that adjacency in $G$ is determined by a (fixe
d) function of the two labels of the endpoints. The size of a labeling sch
eme is the bit length of the longest label\, which we want as small as pos
sible. If $|\\mathcal{C}_n|$ denotes the number of $n$-vertex graphs in $\
\mathcal{C}$\, then any adjacency labeling scheme has size at least $(\\l
og|C_n|)/n$. \n\nFor many classes (e.g.~planar\, bounded twin-width\, bou
nded degeneracy) this lower bound is tight. In 1988 the Implicit Graph Con
jecture (IGC) postulated that any hereditary (closed under induced subgrap
hs) class $\\mathcal{C}$ with $|\\mathcal{C}_n|=2^{O(n\\log n)}$ admits a
labeling scheme of size $\\Theta(\\log n)$\, matching the lower bound. Ha
tami & Hatami recently disproved this\, using the probabilistic method to
construct a hereditary factorial class requiring almost $\\sqrt{n}$ size l
abels.\n\nWe begin with a more gentle introduction to labeling schemes\, b
efore outlining what we think to be the correct reformulation of the IGC:
any hereditary class $\\mathcal{C}$ with $|\\mathcal{C}_n|=n!\\\,2^{O(n)}$
admits a labeling scheme of size $\\Theta(\\log n)$. We prove this under
the additional restriction that the class is weakly sparse (excludes some
fixed bipartite complete graph as a subgraph). We also prove that the conj
ecture holds if one relaxes the size bound to $O(\\log^3 n)$\, improving o
n the previously best-known upper bound of $n^{1-\\Omega(1)}$. \n\nThis i
s joint work with Édouard Bonnet\, Julien Duron\, Viktor Zamaraev & Maksi
m Zhukovskii.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/35/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Daniel Hausmann (University of Liverpool)
DTSTART:20250207T140000Z
DTEND:20250207T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/36
DESCRIPTION:Title: Infinite-duration Games in Formal Methods\nby Daniel Hausmann (U
niversity of Liverpool) as part of University of Birmingham theoretical co
mputer science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbst
ract\nInfinite duration two-player games have been established as a formal
ism for the treatment of decision problems for various temporal logics. Su
ch games can be used to evaluate qualitative temporal properties\, subsumi
ng safety\, reachability\, or general liveness properties\, which are typi
cally given in the form of omega-regular winning conditions.\n\nThis talk
will first give an overview on how omega-regular games are used as a centr
al back-end tool for reactive synthesis (LTL synthesis)\, and for model an
d satisfiability checking for fixpoint logics (such as the modal mu-calcul
us).\n\nSubsequently\, the talk will present recent progress regarding alg
orithms for the analysis of two types of omega-regular games: Emerson-Lei
games and obliging games. In the former\, the winning condition is an arbi
trary Boolean combination of events that should occur infinitely often (or
only finitely often). The latter encode a certain degree of cooperation b
etween the two players.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/36/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Matthew Alan Le Brun (University of Glasgow)
DTSTART:20250228T140000Z
DTEND:20250228T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/37
DESCRIPTION:Title: Multiparty Session Types with a Bang!\nby Matthew Alan Le Brun (
University of Glasgow) as part of University of Birmingham theoretical com
puter science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstr
act\nTypes in programming languages abstract away the specifics of a progr
am to provide a lightweight form of static verification. Multiparty Sessio
n Types (MPST) do just that for message passing programs where many partic
ipants communicate together via a multiparty session. Traditionally\, recu
rsion has been the preferred method of describing infinite computation in
MPST\; in this study\, we investigate the use of replication\, an alternat
ive construct to recursion that denotes a process as one which is infinite
ly available. We introduce MPST!\, a session-typed multiparty process calc
ulus with replication and first-class roles. We find that replication is n
ot an equivalent alternative to recursion in MPST\, and using both constru
cts in one type system in fact allows us to express both context-free prot
ocols and protocols that make interesting use of mutual exclusion and race
s. In this talk\, we will demonstrate the expressiveness of replication in
MPST by example\, observe the mutual non-inclusion result\, and discuss t
he decidability of typechecking.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/37/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rodrigo Nicolau Almeida (ILLC\, University of Amsterdam)
DTSTART:20250404T130000Z
DTEND:20250404T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/39
DESCRIPTION:Title: Heyting algebras one step at a time\nby Rodrigo Nicolau Almeida
(ILLC\, University of Amsterdam) as part of University of Birmingham theor
etical computer science seminar\n\nLecture held in LG23\, Computer Science
.\n\nAbstract\nFor almost 100 years Heyting algebras have been the subject
of intense study\, both as algebraic models for the intuitionistic propos
itional calculus\, IPC\, as well as in connection with point-free topology
and the lambda calculus\, where they appear naturally. A lot of this work
has been assisted by Esakia duality\, which represents such algebras usin
g ordered-topological spaces with a particular structure. Despite this int
ense work\, several basic questions concerning (1) constructions of Heytin
g algebras - especially concerning free algebras\, coproducts and other in
itial-like constructions have remained unanswered or been left outside of
the scope of analysis. In this talk I will survey some recent work on the
duality theory of step-by-step constructions of Heyting algebras and relat
ed structures\, as well as highlight its potential use in attacking some o
pen questions in the study of extensions of intuitionistic logic:\n\nKuzne
tsov's problem: whether every variety of Heyting algebras is generated by
its complete algebras.\nPitts and Pataraia’s problem: whether every Heyt
ing algebra arises as the algebra of truth values of an elementary topos.\
nThis talk reports on some ongoing work with Mamuka Jibladze.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/39/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rini Banerjee (University of Cambridge)
DTSTART:20250214T140000Z
DTEND:20250214T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/40
DESCRIPTION:Title: Fulminate: Testing CN Separation-Logic Specifications in C\nby R
ini Banerjee (University of Cambridge) as part of University of Birmingham
theoretical computer science seminar\n\nLecture held in LG23\, Computer S
cience.\n\nAbstract\nSystems code (e.g. operating systems\, hypervisors) f
orms a crucial part of our everyday computing infrastructure\, with much o
f it written in C/C++. Virtually all C/C++ programs involve manual memory
management via pointers\, leading to complex ownership patterns that are d
ifficult to describe formally. Separation logic has become an important t
ool for capturing and reasoning about these ownership patterns\, forming t
he basis of several static analysis and proof tools (e.g. CN [1]\, a verif
ication tool for C). However\, little work has been done on testing separa
tion logic specifications in concrete execution\, since at first glance\,
separation-logic formulas are hard to evaluate in a reasonable amount of t
ime. In this talk I describe our work on Fulminate [2]\, a tool for testin
g CN separation-logic specifications on concrete inputs in C.\n\n[1] CN: V
erifying Systems C Code with Separation-Logic Refinement Types. Christophe
r Pulte\, Dhruv C. Makwana\, Thomas Sewell\, Kayvan Memarian\, Peter Sewel
l\, Neel Krishnaswami. POPL 2023.\n[2] Fulminate: Testing CN Separation-Lo
gic Specifications in C. Rini Banerjee\, Kayvan Memarian\, Dhruv Makwana\,
Christopher Pulte\, Neel Krishnaswami\, Peter Sewell. POPL 2025.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/40/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Karteek Sreenivasaiah (University of Liverpool)
DTSTART:20250221T140000Z
DTEND:20250221T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/41
DESCRIPTION:Title: Unconditional lower bounds for Orthogonal Vectors\nby Karteek Sr
eenivasaiah (University of Liverpool) as part of University of Birmingham
theoretical computer science seminar\n\nLecture held in LG23\, Computer Sc
ience.\n\nAbstract\nFine-grained complexity is a modern area of computer s
cience that has been successful in identifying problems that are bottlneck
s to computation within finer levels of polynomial time. One such function
is Orthogonal Vectors (OV) -- given two tuples A and B of n Boolean vecto
rs\, each of dimension d\, decide if there exists a vector in A and a vect
or in B such that they are othogonal.\n\nIt has been established that seve
ral important functions have faster algorithms only if OV does. In very in
formal terms\, an instance of OV is hiding inside these functions. Hence c
omputing these functions essentially involves computing the OV instance em
bedded inside them. \n\nA central conjecture in fine-grained complexity kn
own as the "OV-conjecture" states that OV cannot be solved in time $n^{2-\
\epsilon}$ for any $\\epsilon > 0$. In this talk\, we will prove the OV co
njecture for a restricted model of depth-3 Boolean circuits. The focus of
the talk is on the combinatorial ideas that are used to show such an uncon
ditional lower bound. No background in circuits or fine-grained complexity
is assumed.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/41/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Caterina Viola (University of Catania)
DTSTART:20250321T140000Z
DTEND:20250321T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/42
DESCRIPTION:Title: Algebraic Approach to Approximation\nby Caterina Viola (Universi
ty of Catania) as part of University of Birmingham theoretical computer sc
ience seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nWha
t makes a computational problem easy or hard to solve approximately? In th
is talk\, we introduce valued promise CSPs (valued PCSPs)\, a broad class
that includes CSPs\, valued CSPs\, and various approximation problems. We
present the key algebraic structures that capture their complexity and ena
ble polynomial-time reductions. Using illustrative examples\, we show how
this framework unifies known results and offers new insights into computat
ional hardness.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/42/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Mario Román (University of Oxford)
DTSTART:20250307T140000Z
DTEND:20250307T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/43
DESCRIPTION:Title: String Diagrams for Premonoidal Categories\nby Mario Román (Uni
versity of Oxford) as part of University of Birmingham theoretical compute
r science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\
nPremonoidal categories are monoidal categories without the interchange la
w while effectful categories are premonoidal categories with a chosen mono
idal subcategory of interchanging morphisms. In the same sense that string
diagrams\, pioneered by Joyal and Street\, are an internal language for m
onoidal categories\, we will see how string diagrams with an added "runtim
e object"\, pioneered by Alan Jeffrey\, are an internal language for effec
tful categories and can be used as string diagrams for effectful\, premono
idal\, and Freyd categories. This talk is partly based on joint work with
Paweł Sobociński.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/43/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Vincent Moreau (IRIF\, Paris)
DTSTART:20250328T140000Z
DTEND:20250328T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/44
DESCRIPTION:Title: Profinite lambda-terms and higher-order regular languages\nby Vi
ncent Moreau (IRIF\, Paris) as part of University of Birmingham theoretica
l computer science seminar\n\nLecture held in LG23\, Computer Science.\n\n
Abstract\nFor several years now\, there has been a growing connection betw
een automata theory and λ-calculus\, in terms of syntax\, semantics and l
ogic. The notion of language of λ-terms recognized by a cartesian closed
category\, introduced by Salvati\, is a fundamental contribution to this c
onvergence as it generalizes to the higher-order the usual regular languag
e of finite words and trees.\n\nWe present recent advances on that theme.
First\, we show that the notion of higher-order regular language is robust
\, by providing a natural criterion for cartesian closed categories to rec
ognize exactly these languages. To achieve this\, we establish a close lin
k with the implicit automata programme of Nguyen and Pradic. Second\, we e
xplain how higher-order regular languages assemble into a fibration and wh
at this means in terms of quantifiers in the style of MSO. Third\, we intr
oduce profinite λ-terms\, a higher-order generalization of the notion of
profinite word related to regular languages by Stone duality. These assemb
le into a cartesian closed category which verifies an adequate universal p
roperty with respect to finite models\, justifying the denomination of pro
finite λ-calculus.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/44/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Geoff Sutcliffe (University of Miami)
DTSTART:20250509T130000Z
DTEND:20250509T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/45
DESCRIPTION:Title: The TPTP World - Infrastructure for Automated Reasoning\nby Geof
f Sutcliffe (University of Miami) as part of University of Birmingham theo
retical computer science seminar\n\nLecture held in LG23\, Computer Scienc
e.\n\nAbstract\nThe TPTP World is the established infrastructure used by t
he Automated Theorem Proving (ATP) community for research\, development\,
and deployment of ATP systems. The data\, standards\, and services provide
d by the TPTP World have made it easy to develop\, evaluate\, and deploy A
TP technology. This talk and tutorial reviews the core features of the TPT
P World\, describes key services of the TPTP World\, and presents some suc
cessful applications. The use of ATP as the reliable substrate to subsymbo
lic AI systems (e.g.\, LLMs)\, to form neurosymbolic AI systems\, is revie
wed.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/45/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rahaleh Jalali (University of Bath)
DTSTART:20250516T130000Z
DTEND:20250516T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/46
DESCRIPTION:Title: Skolemization and the logic of quantifier shifts\nby Rahaleh Jal
ali (University of Bath) as part of University of Birmingham theoretical c
omputer science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbs
tract\nSkolemization is a method to remove strong quantifiers (i.e.\, posi
tive occurrences of the universal quantifier and negative occurrences of t
he existential quantifier) from a first-order formula and replace them wit
h fresh function symbols. It is a well-known fact that Skolemization is so
und and complete with respect to the classical predicate logic\, CQC. At t
he same time\, this is not the case for the intuitionistic predicate logic
\, IQC. In this talk\, we consider the three formulas known as the "quanti
fier shifts"\, which are provable in CQC but not in IQC. One may suspect t
hat the failure of the quantifier shifts is why Skolemization fails in IQC
. Therefore\, asking what happens if we add the quantifier shifts to IQC i
s natural. Does the resulting logic have Skolemization? If not\, for which
class of formulas does the Skolemization hold? These questions build the
motivation of the present research study that investigates the logic of qu
antifier shifts and its Skolemization. This is a joint work with Matthias
Baaz\, Rosalie Iemhoff\, and Mariami Gamsakhurdia.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/46/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sayan Bhattacharya (University of Warwick)
DTSTART:20250523T130000Z
DTEND:20250523T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/47
DESCRIPTION:Title: Vizing's Theorem in Near-Linear Time\nby Sayan Bhattacharya (Uni
versity of Warwick) as part of University of Birmingham theoretical comput
er science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract
\nA textbook theorem by Vizing from the 1960s guarantees that any graph wi
th n nodes\, m edges and maximum degree \\Delta admits a proper edge color
ing with only (\\Delta+1) colors. But\, how quickly can we compute such a
(\\Delta+1)-coloring in a given input graph? We present the first near-lin
ear time algorithm for this fundamental problem. Our algorithm runs in onl
y O(m \\log \\Delta) time\; this matches the longstanding O(m \\log \\Delt
a) time bound for computing a \\Delta-edge coloring in bipartite graphs.\n
\nJoint work with Sepehr Assadi\, Soheil Behnezhad\, Martin Costa\, Shay S
olomon and Tinayi Zhang.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/47/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dylan McDermott (University of Oxford)
DTSTART:20250530T130000Z
DTEND:20250530T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/48
DESCRIPTION:Title: Notions of presentation for graded monads\nby Dylan McDermott (U
niversity of Oxford) as part of University of Birmingham theoretical compu
ter science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstrac
t\nMonads\, and their presentations through operations and equations\, are
used to model computations involving effects\, such as mutable state and
nondeterministic choice. When we want to track information about the effec
ts of computations\, for instance in a type-and-effect analysis\, we inste
ad use the more general concept of _graded monad_.\n\nIn this talk I will
discuss notions of presentation for graded monad. There is a notion of gra
ded presentation that appears naturally when we think about what kind of g
raded algebraic structures correspond to graded monads\, and these graded
presentations satisfy analgous properties to those we get in the ungraded
setting. Unfortunately\, it turns out they don't work very well for effect
s of interest. I will therefore introduce a more general notion of _flexib
ly_ graded presentation\, one that better captures the effects. To do this
we have to depart slightly from the usual techniques for doing algebraic
theories\, but I will argue that we do not lose too much by doing so.\n\nT
his talk is based on joint work with Shin-ya Katsumata\, Tarmo Uustalu\, a
nd Nicolas Wu\, described in the following papers:\n Dylan McDermott and
Tarmo Uustalu\, Flexibly graded monads and graded algebras\, MPC 2022\n S
hin-ya Katsumata\, Dylan McDermott\, Tarmo Uustalu and Nicolas Wu\, Flexib
le presentations of graded monads\, ICFP 2022\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/48/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nikhil Mande (University of Liverpool)
DTSTART:20250606T130000Z
DTEND:20250606T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/49
DESCRIPTION:Title: On Kings in Tournaments\nby Nikhil Mande (University of Liverpoo
l) as part of University of Birmingham theoretical computer science semina
r\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nA tournament is
a complete directed graph. These graphs model round-robin tournaments suc
h as the premier league. A king in a tournament is a vertex k such that ev
ery other vertex is reachable by a path of length 1 or 2 from k. It is wel
l known that every tournament has a king\, in particular a maximum out-deg
ree vertex is a king. I will talk about my recent results on the complexit
y of finding a king\, and other variants of winners\, in a tournament. No
technical background will be assumed.\nBased on joint works with Ziad Isma
ili Alaoui\, Manaswi Paraashar\, Swagato Sanyal\, and Nitin Saurabh.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/49/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Parinya Chalermsook (University of Sheffield)
DTSTART:20250620T130000Z
DTEND:20250620T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/50
DESCRIPTION:Title: Extremal Combinatorics Meets Algorithms and Data Structures\nby
Parinya Chalermsook (University of Sheffield) as part of University of Bir
mingham theoretical computer science seminar\n\nLecture held in Aston Webb
Dome Lecture Theatre.\n\nAbstract\nThis talk explores a rich interplay be
tween extremal combinatorics and the analysis of algorithms and data struc
tures. In the first part of the talk\, I will explain how classical Ramsey
theory tightly captures a fundamental question in approximation algorithm
s and how the LP rounding perspectives (techniques that are central in app
roximation algorithms) led to breaking a 6-decade-old extremal bound on re
ctangle coloring. In the second part\, I will discuss the role of extremal
combinatorics in the context of sorting and binary search trees (in parti
cular\, the long-standing dynamic optimality conjecture). In both scenario
s\, such interplay has been crucial in making progress and highlights the
two-way dialogue between the two fields.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/50/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Guillaume Munch-Maccagnoni (INRIA Nantes)
DTSTART:20250627T130000Z
DTEND:20250627T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/51
DESCRIPTION:Title: Resource management in programming\, call-by-push-value\, and ordere
d logic\nby Guillaume Munch-Maccagnoni (INRIA Nantes) as part of Unive
rsity of Birmingham theoretical computer science seminar\n\nLecture held i
n LG23\, Computer Science.\n\nAbstract\nAlthough linear logic was seen as
a source of inspiration for the design of programming languages (promising
to reconcile imperative and functional programming to some\, no less!)\,
the integration of notions of linearity in programming language theory has
been slow. Examples are rarer to come by than meaningful models of effect
ful computation determined by monads\, as are examples that meaningfully m
ix linearity and effects. We propose a new example (which meaningfully ref
ines linear logic\, and meaningfully mixes linearity and effects) whose mo
tivation is to model the notion of resource from the C++ and Rust programm
ing languages. In these languages\, a resource is a value abstraction for
some state which requires that some clean-up action is correctly performed
at a specific moment. These languages show a possible (and in practice wi
dely successful) way to integrate resources with control (e.g. exceptions)
. Similarly\, our model shows how linearity can be combined with control e
ffects such as the exception monad\, exhibiting similar features as C++/Ru
st. The main tool we use is the decomposition of notions of computation in
to adjunctions provided by call-by-push-value (CBPV). Somehow\, this endea
vour requires us to refine the notion of linear CBPV model into an ordered
(i.e. non-commutative) CBPV.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/51/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Antonio Lorenzin (UCL)
DTSTART:20250926T130000Z
DTEND:20250926T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/53
DESCRIPTION:Title: Categories of abstract and noncommutative measurable spaces\nby
Antonio Lorenzin (UCL) as part of University of Birmingham theoretical com
puter science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstr
act\nIn quantum probability\, the category of $C^*$-algebras and completel
y positive unital (cpu) maps is a well-established setting. However\, its
classical side\, given by commutative $C^*$-algebras\, does not contain al
l regular conditional probabilities\, a central concept in classical proba
bility. This shortcoming is due to the inherent topological nature of $C^*
$-algebras\, which ties them to continuous rather than measurable structur
es.\n\nTo address this\, we investigate what noncommutative (or quantum) m
easurable spaces should be\, by establishing adjunctions and equivalences
between special classes of $C^*$-algebras and cpu maps and categories of m
easurable spaces and Markov kernels. On the classical side\, these can be
equivalently described by Boolean σ-algebras (also known as abstract meas
urable spaces). Moreover\, our operator-algebraic analysis equips these st
ructures with a generalized notion of Markov kernels\, realized as POVMs.
\n\nUltimately\, we obtain a categorical framework in which both classical
and quantum probability coexist\, and the classical side has regular cond
itional probabilities.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/53/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nachi Valliappan (University of Edinburgh)
DTSTART:20251003T130000Z
DTEND:20251003T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/54
DESCRIPTION:Title: Lax modal lambda calculi\nby Nachi Valliappan (University of Edi
nburgh) as part of University of Birmingham theoretical computer science s
eminar\n\nLecture held in LC-UG10 Murray Learning Centre.\n\nAbstract\nInt
uitionistic modal logic (IML) is the study of extending intuitionistic pro
positional logic with modal operators such as the box and diamond modaliti
es. Advances in IML have led to a plethora of useful applications in progr
amming languages via the development of corresponding type theories with m
odalities. Until recently\, IMLs with diamonds had been misunderstood as s
omewhat peculiar and unstable\, causing the development of type theories w
ith diamonds to lag behind type theories with boxes.\n\nIn this talk\, I w
ill present a family of typed-lambda calculi corresponding to sublogics of
a peculiar IML with diamonds known as Lax logic. These calculi provide a
modal logical foundation for strong functors in functional programming and
make it possible to formalize the connection between possible-world seman
tics for IMLs and categorical semantics for corresponding lambda calculi.
I hope to end this talk with a summary of what I’ve learnt from IML lite
rature and how it has inspired me to think about semantics of modalities i
n programming languages beyond boxes and diamonds. \n\nA draft article on
this topic can be found here: $\\url{https://nachivpn.me/lmlc.pdf}$\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/54/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jim de Groot (University of Bern)
DTSTART:20251017T130000Z
DTEND:20251017T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/55
DESCRIPTION:Title: Intuitionistic monotone modal logic\nby Jim de Groot (University
of Bern) as part of University of Birmingham theoretical computer science
seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nWe intro
duce a monotone modal analogue of the intuitionistic (normal) modal logic
IK using a translation into a suitable (intuitionistic) first-order logic.
We axiomatise the logic and give a semantics by means of intuitionistic n
eighbourhood models\, which are models whose neighbourhoods can change whe
n moving along the intuitionistic accessibility relation. We compare the r
esulting logic with other intuitionistic monotone modal logics to find con
servativity results resembling those of the logics between CK and IK.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/55/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ohad Kammar (University of Edinburgh)
DTSTART:20251024T130000Z
DTEND:20251024T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/56
DESCRIPTION:Title: Modular abstract syntax trees (MAST) – substitution tensors with s
econd-class sorts\nby Ohad Kammar (University of Edinburgh) as part of
University of Birmingham theoretical computer science seminar\n\nLecture
held in LG23\, Computer Science.\n\nAbstract\nWe adapt Fiore\, Plotkin\, a
nd Turi's treatment of abstract syntax with binding\, substitution\, and h
oles to account for languages with second-class sorts. These situations in
clude programming calculi such as the Call-by-Value λ-calculus (CBV) and
Levy's Call-by-Push-Value (CBPV). Prohibiting second-class sorts from appe
aring in variable contexts means the presheaf of variables is no longer a
left-unit for Fiore et al's substitution tensor product. We generalised th
eir development to associative and right-unital skew monoidal categories.
We reuse much of the development through skew bicategorical arguments. In
ongoing work\, we replace the skew monoidal structure with ordinary monoid
al structure by recourse to substitution modules instead of substitution m
onoids.\n\nWe apply the resulting theory in two scenarios. We employ the m
athematical theory to circumvent the expression problem when proving subst
itution lemmata for varieties of CBV denotational semantics modularly. We
employ a computational implementation of the theory to circumvent the expr
ession problem when implementing intrinsically-typed foreign-function inte
rfaces for the 29 theories of SMTLIB.\n\nJoint work with Marcelo Fiore\, K
ajetan Granops\, Mihail-Codrin Iftode\, Georg Moser\, and Sam Staton.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/56/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bruno Cavalar (University of Oxford)
DTSTART:20251031T140000Z
DTEND:20251031T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/57
DESCRIPTION:Title: Monotone Circuit Complexity of Matching\nby Bruno Cavalar (Unive
rsity of Oxford) as part of University of Birmingham theoretical computer
science seminar\n\nLecture held in Aston Webb G33.\n\nAbstract\nWe show th
at the perfect matching function on n-vertex graphs requires monotone circ
uits of exponential size. This improves on the quasipolynomial lower bound
of Razborov (1985). Our proof uses the standard approximation method toge
ther with a new sunflower lemma for matchings.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/57/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Matteo Acclavio (University of Sussex)
DTSTART:20251107T140000Z
DTEND:20251107T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/58
DESCRIPTION:Title: Dealing with Concurrency in Dynamic Logic\nby Matteo Acclavio (U
niversity of Sussex) as part of University of Birmingham theoretical compu
ter science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstrac
t\nDynamic logic is a versatile framework for reasoning about properties o
f programs. It extends classical logic with modalities quantifying proposi
tions based on program executions. In this context\, dealing with concurre
ncy has proved problematic\, mainly because of the difficulty of capturing
interleaving. In recent work\, we developed a new framework we call opera
tional propositional dynamic logic (OPDL). The key feature of our approach
is to consider programs and their operational semantics as a parameter of
the logic\, allowing us to overcome some limitations of traditional propo
sitional dynamic logic (PDL).\n\nIn this talk\, I will give motivations fo
r this work\, and I will explain the technical aspects of proof of adequac
y –relying on a proof of cut-elimination for a finitely branching non-we
llfounded sequent calculus for PDL. After discussing how traditional PDL c
an be seen as specific instance of OPDL\, I will show two representative c
ases of concurrent programming languages: the Calculus of Communicating Sy
stems (CCS)\, where concurrency arises from parallel composition\, and Cho
reographic Programming\, where it arises from out-of-order execution.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/58/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Anupam Das (University of Birmingham)
DTSTART:20251128T140000Z
DTEND:20251128T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/59
DESCRIPTION:Title: Right-linear structures: decomposing the theory of (omega-)regular l
anguages via fixed points\nby Anupam Das (University of Birmingham) as
part of University of Birmingham theoretical computer science seminar\n\n
Lecture held in LG23\, Computer Science.\n\nAbstract\nIn the second half o
f the 20th century various theories of regular expressions were proposed\,
eventually leading to the notion of a Kleene Algebra (KA). Kozen and Krob
independently proved the completeness of KA for the model of regular lang
uages\, a now celebrated result that has been refined and generalised over
the years. In recent years proof theoretic approaches to regular language
s have been studied\, providing alternative routes to metalogical results
like completeness and decidability.\n\nIn this talk I will present a new a
pproach from a different starting point: finite state automata. A notation
for non-deterministic finite automata is readily obtained via expressions
with least fixed points\, leading to a theory of right-linear algebras (R
LA). RLA is strictly more general than KA\, e.g. admitting ω-regular lang
uages as a model too\, and enjoys a simpler proof theory than KA. This all
ows us to recover (more general) metalogical results in a robust way\, com
bining techniques from automata\, games\, and cyclic proofs. In particular
\, our development exposes a novel factorisation of the completeness for K
A\, controlling the use of multiplication.\n\nThis talk is based on severa
l joint works with Abhishek De.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/59/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tikhon Pshenitsyn (Steklov Mathematical Institute)
DTSTART:20251010T130000Z
DTEND:20251010T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/60
DESCRIPTION:Title: First-order linear logic and graph languages\nby Tikhon Pshenits
yn (Steklov Mathematical Institute) as part of University of Birmingham th
eoretical computer science seminar\n\nLecture held in LG23\, Computer Scie
nce.\n\nAbstract\nLinear logic provides a way of reasoning about resources
or actions. One of its prominent applications is in linguistics: words an
d word collocations can be regarded as resources that are combined into se
ntences according to certain composition rules. The Lambek calculus—also
known as noncommutative multiplicative intuitionistic linear logic—serv
es this purpose by enabling one to generate formal languages. Pentus (1993
) proved that grammars based on the Lambek calculus generate exactly conte
xt-free languages. Later\, Pentus (1995) showed that the Lambek calculus i
s sound and complete with respect to formal language models. These results
establish a strong connection between linear logic and the formal languag
e theory.\n\nThis talk begins with an introduction to linear logic and the
Lambek calculus. After that we turn to discussion of first-order linear l
ogic and its recently established connection to the formal language theory
. It turns out that first-order linear logic can be used to generate graph
languages in the same way the Lambek calculus is used to generate string
languages. Graph grammars based on first-order linear logic generate a wid
er class of languages than graph context-free languages\; the former is cl
osed under intersection and it subsumes linear-time graph transformation s
ystems. In the final part of the talk\, we briefly discuss model-theoretic
aspects of first-order linear logic\, showing that its negative fragment
is sound and complete w.r.t. graph language semantics.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/60/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Thomas Sauerwald (University of Cambridge)
DTSTART:20251003T143000Z
DTEND:20251003T153000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/61
DESCRIPTION:Title: Balanced Allocations: The Power of Choice versus Noise\nby Thoma
s Sauerwald (University of Cambridge) as part of University of Birmingham
theoretical computer science seminar\n\nLecture held in Watson Lecture The
atre B.\n\nAbstract\nIn the balanced allocation problem we wish to allocat
e m balls (jobs) into n bins (servers) by allowing each ball to choose fro
m some bins sampled uniformly at random. The goal is to maintain a small g
ap between the maximum load and average load. For the one-choice protocol\
, where each ball is allocated to a random bin\, the gap diverges for larg
e m. However\, for the two-choice protocol\, where each ball samples two b
ins and is placed in the least loaded of the two\, it was shown more than
20 years ago that the gap is only O(log log n) for all m. This dramatic im
provement is widely known as ``power of two choices’’\, and similar ef
fects have been observed in hashing and routing.\n\nIn this talk\, we will
present new results in settings where the load information is restricted
or noisy. For example\, the queried load information of bins might be (i)
outdated\, (ii) subject to some adversarial or random perturbation or (iii
) only retrievable by binary queries. We also exhibit settings with strong
noise and demonstrate that having more choices can lead to a worse perfor
mance.\n\nThis is based on joint works with Dimitrios Los and John Sylvest
er. More information and some illustrations of the results are also availa
ble under:\n\n$\\url{dimitrioslos.com/research/phd-thesis/index.html}$\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/61/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Paul Taylor (University of Birmingham)
DTSTART:20251121T140000Z
DTEND:20251121T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/62
DESCRIPTION:Title: A Categorical Replacement for Replacement\nby Paul Taylor (Unive
rsity of Birmingham) as part of University of Birmingham theoretical compu
ter science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstrac
t\nIt is more than 50 years since Lawvere and Tierney introduced elementar
y toposes as an alternative to (bounded) Zermelo set theory and since then
the bulk of mainstream mathematics has been formulated in it. However\, t
here are some constructions such as iterated functors and gluing that go o
utside this framework\, but can be justified using the Axiom-Scheme of Rep
lacement. Replacement is interesting because it can build skyscrapers from
plans on the ground\, whereas using universes or large cardinals is like
dropping building materials from a satellite.\n\nIt is embarrassing after
all this time that category theory does not have a way of expressing Repla
cement in its native language.\n\nIt is a well established and powerful di
scipline that is being applied to more and more subjects. It can stand on
its own feet and does not need set-theoretic foundations. The only reason
for giving one is that ZF has acquired an "official" role and has not yet
been shown to be inconsistent.\n\nThe native language of category theory i
s adjunctions\, which are formally equivalent to introduction--elimination
rule-sets in type theory: we create a new connective by asserting that so
me previously defined functor has an adjoint. The powerful cases are when
the adjoint must be defined recursively\, which raises questions of termin
ation.\n\nTo handle this we use an idea from set theory\, but abstracted a
nd generalised using category theory. The proposal is that any well founde
d structure have an extensional reflection\, where relations become coalge
bras for fairly general functors and subsets become factorisation systems.
\n\nCategorical applications of this such as transfinite iteration of func
tors will be considered on a later occasion. In this lecture I will discus
s the categorical ideas and show that the proposal is valid in ZF\, with a
brief introduction to how that is formulated in first order logic and why
unbounded predicates are needed.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/62/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Martin Costa (University of Warwick)
DTSTART:20251114T140000Z
DTEND:20251114T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/63
DESCRIPTION:Title: Nibbling at Long Cycles: Dynamic (and Static) Edge Coloring in Optim
al Time\nby Martin Costa (University of Warwick) as part of University
of Birmingham theoretical computer science seminar\n\nLecture held in LG2
3\, Computer Science.\n\nAbstract\nWe consider the problem of maintaining
a (1 + ε)Δ-edge coloring in a dynamic graph G with n nodes and maximum d
egree at most Δ. The state-of-the-art update time is Oε (polylog(n))\, b
y Duan\, He and Zhang [SODA'19] and by Christiansen [STOC'23].\n\nThe foll
owing natural question arises: What is the best possible update time of an
algorithm for this task? More specifically\, can we bring it all the way
down to some constant (for constant ε)? This question coincides with the
static time barrier for the problem: Even for (2Δ -1)-coloring\, there is
only a naïve O(m log Δ)-time algorithm.\n\nWe answer this fundamental q
uestion in the affirmative\, by presenting a dynamic (1 + ε)Δ-edge color
ing algorithm with poly(1/ε) update time\, provided Δ = Omegaε (polylog
(n)). As a corollary\, we also get the first linear time (for constant ε)
static algorithm for (1 + ε)Δ-edge coloring\; in particular\, we achiev
e a running time of O(m poly(1/ε)).\n\nWe obtain our results by carefully
combining a variant of the Nibble algorithm from Bhattacharya\, Grandoni
and Wajc [SODA'21] with the subsampling technique of Kulkarni\, Liu\, Sah\
, Sawhney and Tarnawski [STOC'22].\n\nThis talk is based on joint work wit
h Sayan Bhattacharya\, Nadav Panski and Shay Solomon.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/63/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dimitrios Economou (University of Cambridge)
DTSTART:20251205T140000Z
DTEND:20251205T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/64
DESCRIPTION:Title: Focusing is CBPV but CBPV is almost focusing\nby Dimitrios Econo
mou (University of Cambridge) as part of University of Birmingham theoreti
cal computer science seminar\n\nLecture held in LG23\, Computer Science.\n
\nAbstract\nHistorically\, focusing arose from the study of proof search i
n linear logic. Call-By-Push-Value (CBPV) instead arose from the study of
computational effects in programming languages. Each of these calculi intr
oduces a notion of duality: between left and right inversion (positive and
negative formulas) for focused sequent calculi\, and between call-by-valu
e and call-by-name (value and computation types) for CBPV. Remarkably\, th
e polarised type structure of these two calculi is absolutely identical. H
owever\, their judgmental structures are quite different\, with focusing h
aving typing contexts of negative (computation) types which is the opposit
e of CBPV’s contexts of value (positive) types. Researchers have puzzled
over their relationship for decades. In this talk\, we clarify the relati
onship. \n\nWe recall standard calculi for intuitionistic focusing and CBP
V\, and give categorical semantics for both. We also give syntactic transl
ations back and forth. We show that the translation from focusing to CBPV
preserves the denotations of terms exactly\, but that the backwards transl
ation introduces double polarity shifts that break focusing. However\, usi
ng a logical relation\, we show that the translation from CBPV to focusing
is adequate.\n\nThis is joint work with Neel Krishnaswami.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/64/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alyssa Renata (Imperial College London)
DTSTART:20251212T140000Z
DTEND:20251212T150000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/65
DESCRIPTION:Title: Stone Duality for Monads\nby Alyssa Renata (Imperial College Lon
don) as part of University of Birmingham theoretical computer science semi
nar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nIn computer s
cience\, monads are often interpreted as representing computation which in
teract with some resource or environment. To what extent can we interpret
arbitrary monads in this way?\n\nTo answer this question\, I will associat
e to each monad its topological behaviour category\, whose objects are und
erstood as states of the environment\, and whose morphisms are transitions
along states. I will also explain how to recover a monad from a topologic
al category\, giving rise to an adjunction between the category of monads
on set and a category of topological categories.\n\nWe interpret this as a
Stone-type adjunction because any Boolean algebra induces a monad of "if-
then-else" programs\, whose behaviour category has space of objects the St
one spectrum\, and the only morphisms are identity. If time permits\, I wi
ll also explain the relationship between our behaviour category and the Za
riski spectrum of commutative rings\, using an abstract framework of spect
ra invented by Diers and Cole.\n\nThis is joint work with Richard Garner.\
n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/65/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sandra Kiefer (Oxford)
DTSTART:20260130T130000Z
DTEND:20260130T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/66
DESCRIPTION:Title: Long-Refinement Graphs\nby Sandra Kiefer (Oxford) as part of Uni
versity of Birmingham theoretical computer science seminar\n\nLecture held
in LG23\, Computer Science.\n\nAbstract\nThe Colour Refinement algorithm
is a classical procedure to detect symmetries in graphs\, whose most promi
nent application is in graph-isomorphism tests. The algorithm evaluates lo
cal information to compute a colouring for the vertices in an iterative fa
shion. \n\nThe number of iterations that the algorithm takes to terminate
is its central complexity parameter. For a long time\, it was an open ques
tion whether graphs that take the maximum theoretically possible number of
Colour Refinement iterations actually exist. My talk will give an overvie
w of the history of long-refinement graphs\, as well as a report on recent
results.\n\nTogether with Brendan McKay I proved the existence of infinit
e families of such long-refinement graphs with degrees 2 and 3\, thereby s
howing that the trivial upper bound on the iteration number of Colour Refi
nement is tight. Recently\, via reverse-engineering\, T. Devini de Mel and
I obtained a complete characterisation of the long-refinement graphs with
small (or\, equivalently\, large) degrees. This yields that that\, with o
ne exception\, the aforementioned families are the only long-refinement gr
aphs with maximum degree at most 3\, and hence that all long-refinement gr
aphs with degree 2 and 3 can be described via compact strings over a very
small alphabet. \n\nThe work with McKay initiated a search for long-refine
ment graphs that are only distinguished in the last iteration of Colour Re
finement before termination. In the talk\, I will present a simple argumen
t to show that such graphs do not exist.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/66/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Fernando Lucatelli Nunes (Birmingham)
DTSTART:20260123T130000Z
DTEND:20260123T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/67
DESCRIPTION:Title: Eilenberg–Moore\, Kleisli and Descent Factorizations\nby Ferna
ndo Lucatelli Nunes (Birmingham) as part of University of Birmingham theor
etical computer science seminar\n\nLecture held in LG23\, Computer Science
.\n\nAbstract\nEvery functor admitting an adjoint gives rise to canonical
factorization results. Classically\,\na functor with a left adjoint factor
s through the category of Eilenberg–Moore algebras of\nthe induced monad
\, while a functor with a right adjoint factors through the category of\nc
oalgebras of the induced comonad. Dually\, Kleisli and co-Kleisli construc
tions provide\nfurther universal factorizations. \nEvery function admits
an image factorization. The lax analogue of this factorization is\nthe mai
n subject of this talk. Working in a suitable 2-categorical setting with o
pcomma\nobjects and pushouts\, every morphism admits a 2-dimensional coker
nel diagram which\, in\nthe presence of descent objects\, induces a canoni
cal descent factorization. This canonical\ndescent factorization can\, and
should\, be regarded as a lax version of the image factorization. \nThis
lax image factorization\, called lax semantic factorization\, subsumes th
e classical\nEilenberg–Moore and Kleisli factorizations. In particular\,
it yields a novel result even in the\ncase of the 2-category Cat of categ
ories\, which is described below. \nEvery functor has a lax semantic fact
orization. When a functor has a left adjoint\, the\nlax semantic factoriza
tion (lax image factorization) coincides with the Eilenberg–Moore\nfacto
rization\; when it has a right adjoint\, it coincides with the coalgebraic
factorization. \nThis work establishes another connection between monadi
city and descent theory\, providing a formal counterpart to the classical
Bénabou–Roubaud theorem and leading to a\ngeneral monadicity theorem.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/67/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Giacomo Tendas (Manchester)
DTSTART:20260206T130000Z
DTEND:20260206T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/68
DESCRIPTION:Title: Logic internal to a monoidal closed category\nby Giacomo Tendas
(Manchester) as part of University of Birmingham theoretical computer scie
nce seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nIn th
is talk I will explain how one can define notions of language and theory i
nternal to a given (and sufficiently nice) category V endowed with a tens
or product. My motivation for this comes from enriched category theory\,
where we use these theories on V to classify certain important classes of
categories enriched over V. For the purposes of this talk\, I will focus
on how the internal logic is defined (ignoring the enriched categorical as
pects) and give several examples that hopefully will convince you of its u
sefulness. Important instances of V that I will discuss are the category o
f Posets\, that of Metric spaces\, and that of Small Categories.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/68/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Rice (University of Edinburgh)
DTSTART:20260213T130000Z
DTEND:20260213T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/69
DESCRIPTION:Title: A continuation monad for quantum effects in recursive programs\n
by Alex Rice (University of Edinburgh) as part of University of Birmingham
theoretical computer science seminar\n\nLecture held in LG23\, Computer S
cience.\n\nAbstract\nThe semantics of pure quantum programs is well unders
tood\, and we have many tools for working with them. However\, many modern
quantum computing techniques\, such as variational algorithms\, quantum e
rror correction\, and repeat-until-success circuits\, require hybrid quant
um-classical features\, where the semantics are not as clear.\n\n\nIn this
talk\, I will represent these hybrid programs as classical programs which
can operate on quantum data by a computational effect. We show that for n
on-recursive programs\, this effect can be described by so-called quantum
instruments\, by showing that these devices can be given a monad structure
. The rest of the talk will then explore our path to generalising this mon
ad to the category of complete partial orders\, which we desire for descri
bing the semantics of recursive hybrid programs. We note similarities to t
he probabilistic power-domain monad\, which has its multiplication defined
using an integral\, and I will explore our attempts to find a suitable in
tegral construction in our non-commutative setting. I will then present ou
r solution based on continuations\, which effectively bypasses the integra
l construction by instead axiomatising the properties we require from it.\
n\nI will assume no knowledge of quantum computing.\n\nJoint work with Rob
ert Booth\, Dominik Leichtle\, and Kim Worrall\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/69/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nihil Shah (University of Cambridge)
DTSTART:20260220T130000Z
DTEND:20260220T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/70
DESCRIPTION:Title: No-go theorems for distributive laws: directed containers vs. unifor
m sampling\nby Nihil Shah (University of Cambridge) as part of Univers
ity of Birmingham theoretical computer science seminar\n\nLecture held in
LG23\, Computer Science.\n\nAbstract\nMonads model effectful computation\,
comonads model folding with a context. Given a comonad W and a monad M\,
when can two computations WA -> MB and WB -> MC be composed? Power and Wat
anabe demonstrate that the existence of a mixed distributive law WM -> MW
gives a sufficient condition for obtaining a biKleisli category where such
morphisms can be composed. In this talk\, I will demonstrate that\, for a
wide class of (co)monads on the category of sets\, such laws do not exist
. I first show that\, on the category of sets\, there is no mixed distribu
tive law of the non-empty list comonad over the powerset monad. We then ge
neralise the comonad demonstrating that a directed container W has a distr
ibutive law over the powerset monad M if and only if W is a coreader comon
ad. Finally\, we generalise this no-go theorem to all monads over the cate
gory of sets which have a meaningful notion of "uniform sampling". If I ha
ve time\, I will also go over transfer theorems which enable lifting these
no-go theorems over Set to related (co)monads on a different category.\n\
nThis talk is derived from my previous joint work with Amin Karamlou appea
ring in LICS 2024 (https://doi.org/10.1145/3661814.3662137).\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/70/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Elaine Pimentel (University College London)
DTSTART:20260227T130000Z
DTEND:20260227T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/71
DESCRIPTION:Title: Bilateralism with incompatible proofs and refutations\nby Elaine
Pimentel (University College London) as part of University of Birmingham
theoretical computer science seminar\n\nLecture held in LG23\, Computer Sc
ience.\n\nAbstract\nLogical bilateralism challenges traditional concepts o
f logic by treating assertion and denial as independent yet opposed acts.
While initially devised to justify classical logic\, its constructive vari
ants show that both acts admit intuitionistic interpretations. We will pre
sent a bilateral system where a formula cannot be both provable and refuta
ble without contradiction\, offering a framework for modelling\nmathematic
al proofs and refutations that exclude inconsistency.\nWe formalise the lo
gic via a bilateral natural deduction system with the desirable proof-theo
retic properties of normalisation\, subformula property and consistency\,
together with a base-extension semantics grounded in explicit proofs and r
efutations. Finally\, refutation is shown to coincide with Nelson's constr
uctive falsity\, extending intuitionistic logic for constructive epistemic
reasoning.\n\nThis is a joint work with Victor Barroso-Nascimento and Mar
ia Osório\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/71/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Mrudula Balachander (University of Birmingham)
DTSTART:20260306T130000Z
DTEND:20260306T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/72
DESCRIPTION:Title: Towards practical synthesis based on automata learning and succinct
representations\nby Mrudula Balachander (University of Birmingham) as
part of University of Birmingham theoretical computer science seminar\n\nL
ecture held in LG23\, Computer Science.\n\nAbstract\nReactive systems cont
inuously interact with their environment in real-time\, requiring high sta
ndards of correctness\, reliability\, and efficiency. Designing such syste
ms is challenging due to their inherent complexity and the high risk of un
expected behavior or severe failures arising from unforeseen interactions
and\ntiming constraints. Therefore\, rigorous formal methods and verificat
ion are needed to improve the reliability of reactive systems and ensure t
heir correctness. The synthesis problem goes a step further and aims to au
tomate the construction of reactive systems that are guaranteed to meet a
given specification\, typically expressed as logical formulas. This disser
tation advances the field of reactive system synthesis along two main them
es.\n\nFirst\, we address the limitations of automatic LTL synthesis by in
troducing “LTL synthesis with hints” — a novel variant of the LTL sy
nthesis problem that incorporates user guidance in the form of traces to s
teer synthesis algorithms toward more practical and efficient solutions. B
y generalizing the user-provided example traces\, our approach combines pa
ssive learning techniques with existing LTL synthesis algorithms to bridge
the gap between abstract specifications and real-world implementations\,
as demonstrated through an implementation and a series of case studies.\n\
nSecond\, we investigate efficient and effective representations for contr
ollers. Traditional LTL synthesis algorithms output large finite-state Mea
ly machines. To address the need for concise yet efficient representation\
, we explore the class of register automata\, which are finite state machi
nes equipped with registers\, recognising the class of regular languages o
ver infinite alphabets. Our work introduces a novel variant of determinist
ic register automata\, namely Register Automata with Permutations (pDRA)\,
which aims to strike a balance between succinctness and computational eff
iciency. Additionally\, we provide a Myhill–Nerode-like characterisation
that enables the construction of canonical minimal representations. Furth
ermore\, we present a polynomial-time passive learning algorithm for a sub
class of these automata\, demonstrating the efficient identification of th
is class in the limit [63].\n\nTogether\, these contributions enhance the
practicality and scalability of synthesising reactive systems through LTL
specifications\, paving the way for more robust and manageable implementat
ions in real-world applications.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/72/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Pedro Azevedo De Amorim (University of Bath)
DTSTART:20260313T130000Z
DTEND:20260313T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/73
DESCRIPTION:Title: A 2-categorical theory of logical relations\nby Pedro Azevedo De
Amorim (University of Bath) as part of University of Birmingham theoretic
al computer science seminar\n\nLecture held in LG23\, Computer Science.\n\
nAbstract\nLogical relations are a key tool in the semanticist's toolkit.
They play a central role in proofs of adequacy\, in characterizing definab
ility\, and in comparing different interpretations of the same computation
al effect. From a denotational perspective\, logical relations are elegant
ly captured by "fibrations for logical relations". These are Grothendieck
fibrations which strictly preserve the interpretation of types. This theor
y is well-developed for models of the simply-typed lambda calculus and mon
adic-style CBV languages with effects\, but it is not obvious how to exten
d it to other kinds of modal calculi.\n\nIn this talk I will outline the e
xisting theory\, then show how taking a 2-categorical perspective leads na
turally to a mathematically-justified definition of fibration---and hence
logical relations---for a wide variety of modal languages\, including Levy
's call-by-push-value.\n\nNo prior knowledge of 2-category theory or fibra
tions will be assumed.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/73/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Silvia Butti (King's College London)
DTSTART:20260320T130000Z
DTEND:20260320T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/74
DESCRIPTION:Title: The Weisfeiler–Leman Dimension of Relational Database Queries\
nby Silvia Butti (King's College London) as part of University of Birmingh
am theoretical computer science seminar\n\nLecture held in LG23\, Computer
Science.\n\nAbstract\nIn this work we investigate the expressive power of
the k-variable counting logic C^k on relational structures without arity
constraints and its implications for database query languages. \n\nExistin
g results are limited to graphs or to C^2. In our setting\, we consider th
e operation of a relational version of the Weisfeiler-Leman (WL) algorithm
on structures of arbitrary rank. The (k-1)-dimensional WL algorithm is kn
own to have the same expressive power as C^k\, and\, through this link\, t
he WL dimension is an established measure in descriptive complexity theory
. Specifically\, the WL dimension of a query \\varphi denotes the minimum
dimension of the WL algorithm that distinguishes relational structures wit
h different numbers of answers to \\varphi. \n\nOur central technical cont
ribution is the introduction and analysis of a novel Cai-Fürer-Immerman t
ype of construction for general relational structures. Building on this\,
our results are threefold.\nFirst\, we determine the WL dimension of full
conjunctive queries over arbitrary signatures\, and we provide bounds on i
t for general conjunctive queries. Second\, we show that the number of ans
wers to a conjunctive query of WL dimension k in a relational database D c
an be determined from the final labelling that k-WL computes on D. Third\,
by applying our results to Datalog\, we obtain novel bounds on the expres
sivity of Datalog queries.\n\nJoint work with A. Göbel\, L. A. Goldberg\,
S. Kiefer\, M. Lanzinger\, and M. Roth\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/74/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nicholas Pischke (University of Bath)
DTSTART:20260327T130000Z
DTEND:20260327T140000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/75
DESCRIPTION:Title: An overview of proof mining and probability theory\nby Nicholas
Pischke (University of Bath) as part of University of Birmingham theoretic
al computer science seminar\n\nLecture held in LG23\, Computer Science.\n\
nAbstract\nOn the surface\, the theory of probability measures requires th
e use of proof-theoretically strong principles to already develop some of
the most basic notions. Contrary to these apparent limitations\, an approa
ch for extending the program of proof mining to this area has recently bee
n proposed. This approach\, which is fundamentally based on the use of pro
bability contents (i.e.\, finitely additive [0\, 1]-valued functions defin
ed on algebras of sets)\, has proven to be widely effective based on a ran
ge of new case studies presented in the last years. In this talk\, we give
a short overview of both the theoretical work that supports this endeavou
r\, as well as recent applications to stochastic analysis and optimization
which rely on these methods. The talk is based on various (joint) works\,
in collaboration with Morenikeji Neri\, Paulo Oliva and Thomas Powell.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/75/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dmitriy Zhuk (Charles University)
DTSTART:20260410T120000Z
DTEND:20260410T130000Z
DTSTAMP:20260419T023937Z
UID:TheoryCSBham/76
DESCRIPTION:Title: Quantified Constraint Satisfaction Problem: Towards the classificati
on of complexity\nby Dmitriy Zhuk (Charles University) as part of Univ
ersity of Birmingham theoretical computer science seminar\n\nLecture held
in LG23\, Computer Science.\n\nAbstract\nThe Quantified Constraint Satisfa
ction Problem (QCSP) generalizes the\nConstraint Satisfaction Problem (CSP
) by allowing both existential and\nuniversal quantifiers. Formally\, the
QCSP over a constraint language\n$\\Gamma$ asks to evaluate a sentence of
the form\n\\[\n \\forall x_1 \\exists y_1 \\forall x_2 \\exists y_2 \\d
ots\n \\forall x_n \\exists y_n \\ (R_{1}(\\dots) \\wedge \\dots \\wedg
e R_{s}(\\dots))\,\n\\]\nwhere $R_1\,\\dots\,R_s$ are relations from $\\Ga
mma$. While CSP remains in\nNP for any $\\Gamma$\, QCSP can be PSPACE-hard
\, as witnessed by Quantified\n3-Satisfiability or Quantified Graph 3-Colo
uring. Moreover\, in 2018 we\ndiscovered that for some constraint language
s the QCSP is coNP-complete\,\nDP-complete\, and even $\\Theta_{2}^{P}$-co
mplete. With six complexity\nclasses already appearing\, a full classifica
tion had seemed out of reach.\n\nI will discuss recent results that bring
such a classification within\nsight. These include an elementary proof of
the PGP reduction from QCSP\nto CSP\, a gap theorem between $\\Pi_{2}^{P}$
and PSPACE with a criterion\nfor PSPACE-hardness\, and the construction o
f a constraint language whose\nQCSP is $\\Pi_{2}^{P}$-complete --- the mis
sing class.\nTogether\, they\nsupport the conjecture that for any constrai
nt language the QCSP is\ncomplete for one of exactly seven classes:\nP\, N
P\, coNP\, DP\, $\\Theta_2^P$\, $\\Pi_2^P$\, or PSPACE.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/76/
END:VEVENT
END:VCALENDAR