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:20260404T131157Z
UID:TheoryCSBham/1
DESCRIPTION:Title: Turner\, Bird\, Eratosthenes: An Eternal Burning Thread\nb
y Jeremy Gibbons (University of Oxford) as part of University of Birmingha
m theoretical computer science seminar\n\nLecture held in LG23\, Computer
Science.\n\nAbstract\nThe late David Turner had great taste in language de
sign and programming\; the design decisions he made in his languages SASL
\, KRC\, and Miranda over the last 50 years are still influential now. One
example program that he introduced to illustrate lazy evaluation and list
comprehensions in SASL is a one-line recursive “sieve” to generate th
e infinite list of prime numbers.\n\nTurner called this algorithm The Siev
e of Eratosthenes. However\, in a lovely paper “The Genuine Sieve of Era
tosthenes” (JFP\, 2009)\, Melissa O’Neill argued that Turner’s algor
ithm is not faithful to Eratosthenes\, and gave a detailed presentation us
ing priority queues of the real thing. She included a variation by Richard
Bird\, that uses only lists but makes clever use of circular programming.
Bird describes his circular program again in his textbook “Thinking Fun
ctionally with Haskell”\, and sets its proof of correctness as an exerci
se. Unfortunately\, 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 not
ion of “Total Functional Programming” (eg J.UCS\, 2004)\, “designed
to exclude the possibility of non-termination”. He observed that most pr
ograms are already structurally recursive or corecursive\, therefore guara
nteed terminating or productive respectively\, and conjectured that “wit
h more practice we will find this is always true”. Much as I find this i
dea appealing\, I think we are still some way off\, even after 20 years of
“more practice”. I will discuss Bird’s circular Sieve of Eratosthen
es as a challenge problem for Turner’s Total FP.\n
LOCATION:https://stable.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:20260404T131157Z
UID:TheoryCSBham/2
DESCRIPTION:Title: Feferman–Vaught–Mostowski theorems and game comonads\n
by Tomáš Jakl (Czech Academy of Sciences / Czech Technical University) a
s part of University of Birmingham theoretical computer science seminar\n\
nLecture held in LG23\, Computer Science.\n\nAbstract\nIn recent years we
have seen a growing number of examples of model\ncomparison games (such as
pebble games or Ehrenfreucht-Fraisse games)\nbeing encoded semantically\,
as comonads on the class of graphs or\nrelational structures. Apart from
the connections with logic (via the\nmodel comparison games)\, game comona
ds can also express a range of\nimportant parameters in finite model theor
y and combinatorics\, such as\ntree-width and tree-depth.\n\nAfter a brief
overview of the emerging theory of game comonads\, I\nwill present my joi
nt work with Dan Marsden and Nihil Shah. Our main\nfocus are the so-called
Feferman–Vaught-Mostowski-type theorems\, which\nexpress when an operat
ion on models preserves equivalence in a given logic.\n\nProving these the
orems in the comonadic setting amounts to defining\na Kleisli law and chec
king certain smoothness conditions. Surprisingly\,\nthe main ingredient of
our approach is a generalisation of how monoidal\nmonads lift the monoida
l structure to the category of algebras.\nFurthermore\, we also show the r
ole of bilinear maps in this setting and\nhow Johnstone's adjoint lifting
theorem is a special case of all this.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dylan Braithwaite (University of Strathclyde)
DTSTART:20240216T110000Z
DTEND:20240216T120000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/3
DESCRIPTION:Title: Probabilistic Programming with Session Types\nby Dylan Bra
ithwaite (University of Strathclyde) as part of University of Birmingham t
heoretical computer science seminar\n\nLecture held in LG23\, Computer Sci
ence.\n\nAbstract\nStatistical inference algorithms often involve an inter
active flow of information. The fundamental principle behind Bayesian stat
istics can be seen as an interactive process where a model consists of a l
ikelihood function\, which makes a prediction based on some prior knowledg
e\, and later receives observations or updates\, as proposed improvements
to its predictions. Similarly\, the idea of interventions in causal infere
nce has been explained (see Jacobs\, Kissinger and Zanasi) as a kind of fa
ctorisation of a Markov kernel into a kernel with additional input and out
puts\, with certain causal relationship encoding the ideal that the inputs
occur after certain outputs.\n\nInteractive protocols of this sort\, with
interleaved inputs and outputs\, have been modelled in programming langua
ges with session types: type systems for a process calculus which encode e
ncode sequences of sets annotated with input/output information. Typically
semantic models of session types make use of an encoding into linear logi
c\, allowing process specifications to be interpreted in *-autonomous cate
gories. Unfortunately\, categories of probabilistic spaces do not usually
have such structure\, and so are not suitable for as a full model of linea
r logic\, but this structure is far from necessary for modelling simple I/
O sequences. Recently categorical notions of "combs" have been proposed by
several authors as a model for such interactive processes: they provide a
general compositional model for processes with sequenced I/O which can be
constructed over any monoidal category.\n\nIn this talk I will explain ho
w typical operations used in statistical inference algorithms can be succi
nctly represented as operations on combs\, and outline a description of a
simple language with session types to be interpreted in a (multi)category
of combs\, and explore how this can be used as a novel form of probabilist
ic programming language.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/3/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Kavvos (University of Bristol)
DTSTART:20240223T110000Z
DTEND:20240223T120000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/4
DESCRIPTION:Title: Two-dimensional Kripke Semantics\nby Alex Kavvos (Universi
ty of Bristol) as part of University of Birmingham theoretical computer sc
ience seminar\n\nLecture held in G33\, Aston Webb.\n\nAbstract\nThe study
of modal logic has witnessed tremendous development following the introduc
tion of Kripke semantics. However\, recent developments in programming lan
guages and type theory have led to a second way of studying modalities\, n
amely through their categorical semantics. We show how the two correspond.
\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nesta van der Schaaf (University of Edinburgh)
DTSTART:20240301T110000Z
DTEND:20240301T120000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/5
DESCRIPTION:Title: Ordered Locales\nby Nesta van der Schaaf (University of Ed
inburgh) as part of University of Birmingham theoretical computer science
seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nOrder and
topology both abound in mathematics\, often even together. Combined\, the
y form the notion of an ordered topological space. How can this notion be
suitably generalised to the theory of point-free topology? In this talk we
will discuss one possibility\, based on the so-called Egli-Milner relatio
n. To keep the talk accessible\, we start with an introduction to the defi
nition of locales and describe their adjunction with topological spaces. A
fter that\, we show how this adjunction can be extended to certain categor
ies of ordered spaces and the newly introduced ordered locales. To finish
the talk we highlight some ongoing work. First\, we describe how we are us
ing these techniques to study aspects of relativity theory. In particular\
, we describe ingredients for a "causal boundary" construction\, and show
how "domains of dependence" can be recovered as a natural Grothendieck top
ology on ordered locales. Lastly\, time permitting\, we discuss an "intern
al" generalisation of ordered locales. (Based on joint work with Chris Heu
nen and Prakash Panangaden.)\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Charles Grellois (University of Sheffield)
DTSTART:20240308T110000Z
DTEND:20240308T120000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/6
DESCRIPTION:Title: Semantic approaches to verification of functional programs
\nby Charles Grellois (University of Sheffield) as part of University of B
irmingham theoretical computer science seminar\n\nLecture held in LG23\, C
omputer Science.\n\nAbstract\nWhat can the semantics of a program bring wh
en it comes to verification? Almost a decade ago\, during my PhD under the
supervision of Paul-André Melliès\, we showed that the main problem con
sidered in higher-order model-checking could be actually reduced to comput
ing the semantics of the program in some models of linear logic\, enriched
with a modality and a tricky inductive-coinductive fixpoint operator. Dec
idability would follow from the existence of finitary models in which this
"semantic verification procedure" is possible.\n\nAn interesting point in
this approach is that this "practical" problem from verification leads us
to actually consider new and very relevant extensions of the semantics of
linear logic\, notably since the higher-order model-checking problem requ
ires mixing inductive and coinductive reasoning\; but the interplay of pro
grams and alternating tree automata is also surprisingly natural at the li
ght of linear logic.\n\nThe "original" higher-order model-checking problem
was proved decidable by Ong in 2006\; it led to many alternative proofs\,
exploring a vast area of theoretical computer science. I believe that thi
s exploration is far from over\, and will discuss new potential directions
involving cyclic proofs\, infinitary reasoning\, extensional collapses...
\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leo Lobski (University College London)
DTSTART:20240315T110000Z
DTEND:20240315T120000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/7
DESCRIPTION:Title: Towards functorial chemistry: completeness and universality fo
r reaction representation\nby Leo Lobski (University College London) a
s part of University of Birmingham theoretical computer science seminar\n\
nLecture held in LG23\, Computer Science.\n\nAbstract\nOrganic molecules c
an be represented mathematically using labelled graphs [1]. Recently\, the
graph approach to chemistry has been extended to reactions using the tech
niques of graph rewriting [2\,3]. While representing reactions lies at the
heart of mathematical chemistry\, the focus to date has been on the "forw
ard" direction of reaction prediction and composition. The "reverse" direc
tion of discovering reaction pathways to new compounds is\, however\, one
of the main aims of modern chemical engineering. The methodology of this f
ield\, known as retrosynthetic analysis\, is well-established and widely p
ractised [4\,5\,6\,7]\, but has received significantly less mathematical a
ttention.\n\nIn this talk\, I will suggest taking the basic units of retro
synthetic analysis - disconnection rules - as first-class citizens of reac
tion representation. The mathematical and conceptual justification for doi
ng so lies in the fact that both disconnection rules and formalised reacti
ons can be arranged into monoidal categories [8]\, such that there is a mo
noidal functor taking each (composable) sequence of disconnection rules to
a reaction. Our main result shows that\, under a certain axiomatisation o
f the disconnection rules\, the functor is faithful and an opfibration. Th
is implies that every reaction can be decomposed into a sequence of discon
nection rules (universality) in an essentially unique way (completeness).\
n\n[1] D. Bonchev and D.H. Rouvray (eds). Chemical Graph Theory: Introduct
ion and Fundamentals. Abacus Press / Gordon & Breach Science Publishers. 1
991.\n\n[2] J.L. Andersen\, C. Flamm\, D. Merkle\, and P.F. Stadler. Infer
ring chemical 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
. Stadler. An intermediate level of abstraction for computational systems
chemistry. Philos. Trans. R. Soc. 2017.\n\n[4] E.J. Corey and X. Cheng. Th
e logic of chemical synthesis. John Wiley. 1989.\n\n[5] S. Warren and P. W
yatt. Organic synthesis: the disconnection approach. Wiley. 2008.\n\n[6] J
. Clayden\, N. Greeves\, and S. Warren. Organic chemistry. OUP. 2012.\n\n[
7] Y. Sun and N.V. Sahinidis. Computer-aided retrosynthetic design: fundam
entals\, tools\, and outlook. Curr. Opin. Chem. Eng. 2022.\n\n[8] E. Gale\
, L. Lobski\, and F. Zanasi. A Categorical Approach to Synthetic Chemistry
. Theoretical Aspects of Computing - ICTAC. 2023.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Cristina Matache (University of Edinburgh)
DTSTART:20240322T110000Z
DTEND:20240322T120000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/8
DESCRIPTION:Title: Parameterized algebraic theories and applications\nby Cris
tina Matache (University of Edinburgh) as part of University of Birmingham
theoretical computer science seminar\n\nLecture held in LG23\, Computer S
cience.\n\nAbstract\nThe framework of algebraic theories has proved useful
for reasoning equationally about impure computation\, such as state\, non
determinism\, probabilistic choice. In this talk\, I will review parameter
ized algebraic theories\, an extension of algebraic theories that allows f
or binding. I will show how parameterized theories can be used to give an
equational account of scoped effects\, a class of effects that does not fi
t into the plain algebraic framework. Finally\, I will sketch work in prog
ress about axiomatizing dynamic creation of threads using parameterized th
eories.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/8/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Pablo Donato (École Polytechnique)
DTSTART:20240419T100000Z
DTEND:20240419T110000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/9
DESCRIPTION:Title: Deep Inference for Graphical Theorem Proving\nby Pablo Don
ato (École Polytechnique) as part of University of Birmingham theoretical
computer science seminar\n\nLecture held in TBA.\n\nAbstract\nIn this tal
k\, I will summarize my four-year thesis journey focused on designing grap
hical user interfaces (GUIs) for interactive proof construction. Deep infe
rence proof theory guided my approach\, inspiring innovative representatio
ns and interactions with logical entities.\n\nThe first part of the talk w
ill introduce the Proof-by-Action paradigm\, enabling users to construct p
roofs through direct manipulation of the proof state. Actema\, a GUI proto
type for intuitionistic first-order logic\, demonstrates this approach wit
h its drag-and-drop proof tactic grounded in "subformula linking"\, a rece
nt technique based on the calculus of structures.\n\nIn the subsequent dis
cussion\, 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 ic
onic representations of the proof state. This includes the development of
so-called "bubble calculi"\, a family of systems that reframe and extend t
he theory of nested sequents as local rewriting systems. Bubble calculi en
joy a graphical and topological interpretation\, enable efficient sharing
of contexts among subgoals\, and capture both intuitionistic\, dual-intuit
ionistic\, bi-intuitionistic and classical logic in a unified way.\n\nFina
lly\, I will introduce the flower calculus\, an intuitionistic refinement
of C.S. Peirce's theory of existential graphs\, understood as a system for
interactive proof building. It provides more iconic and economical means
of reasoning than bubble calculi\, by exposing a small number of expressiv
e rules that apply to the goals themselves\, removing completely the need
for logical connectives. I will conclude with a demonstration of the Flowe
r Prover\, another prototype of GUI in the Proof-by-Action paradigm\, whos
e actions map directly to the rules of the flower calculus.\n
LOCATION:https://stable.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:20260404T131157Z
UID:TheoryCSBham/10
DESCRIPTION:Title: Higher-Order Weakest Precondition Transformers via a CPS Tran
sformation\nby Satoshi Kura (National Institute of Informatics / Unive
rsity of Oxford) as part of University of Birmingham theoretical computer
science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nW
eakest preconditions are essential notions for program verification. There
are many variations of weakest preconditions\, and their uniform treatmen
t has been studied using category-theoretic notions like monads. In this t
alk\, we consider weakest preconditions for a higher-order functional lang
uage with computational effects and recursion and show that we can syntact
ically compute them via a CPS transformation. We prove our main theorem in
a general setting\, which enables us to instantiate our result to several
problems of program verification. Our result generalises two existing wor
ks on program verification: (1) trace properties and may-/must-reachabilit
y studied by Kobayashi et al. and (2) expected cost analyses studied by Av
anzini et al. We also obtain a new instance of cost moment analyses using
our main theorem.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Igor Carboni Oliveira (University of Warwick)
DTSTART:20240318T130000Z
DTEND:20240318T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/11
DESCRIPTION:Title: Polynomial-Time Pseudodeterministic Construction of Primes\nby Igor Carboni Oliveira (University of Warwick) as part of University
of Birmingham theoretical computer science seminar\n\nLecture held in LG23
\, Computer Science.\n\nAbstract\nA randomized algorithm for a search prob
lem is pseudodeterministic if it produces a fixed canonical solution to th
e search problem with high probability. In their seminal work on the topic
\, Gat and Goldwasser posed as their main open problem whether prime numbe
rs can be pseudodeterministically constructed in polynomial time.\n\nWe pr
ovide a positive solution to this question in the infinitely-often regime.
In more detail\, we give an unconditional polynomial-time randomized algo
rithm $B$ such that\, for infinitely many values of $n$\, $B(1^n)$ outputs
a canonical $n$-bit prime $p_n$ with high probability. More generally\, w
e prove that for every dense property $Q$ of strings that can be decided i
n polynomial time\, there is an infinitely-often pseudodeterministic polyn
omial-time construction of strings satisfying $Q$. This improves upon a su
bexponential-time construction of Oliveira and Santhanam.\n\nOur construct
ion uses several new ideas\, including a novel bootstrapping technique for
pseudodeterministic constructions\, and a quantitative optimization of th
e uniform hardness-randomness framework of Chen and\nTell\, using a varian
t of the Shaltiel-Umans generator.\n\nReference: https://eccc.weizmann.ac.
il/report/2023/076/\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hugo Ferée (IRIF)
DTSTART:20240418T100000Z
DTEND:20240418T110000Z
DTSTAMP:20260404T131157Z
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 theoret
ical computer science seminar\n\nLecture held in Old Gym LG06.\n\nAbstract
\nThe uniform interpolation property in a given logic can be understood as
the definability of propositional quantifiers. We will describe here proo
f-theoretic 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 exist
ing proof). All three proofs are implemented in the Coq proof assistant\,
making the computation of the interpolants effective.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrew Sogokon (Lancaster University)
DTSTART:20240510T100000Z
DTEND:20240510T110000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/14
DESCRIPTION:Title: Inductive Invariants in Continuous Systems\nby Andrew Sog
okon (Lancaster University) as part of University of Birmingham theoretica
l computer science seminar\n\nLecture held in Aston Webb\, WG12.\n\nAbstra
ct\nThe problem of checking whether a set is an inductive invariant is of
fundamental importance to formal safety verification. While the tools requ
ired for this problem in the typical discrete setting are rather straightf
orward and quite standard in computer science\, the situation is markedly
different in continuous systems (i.e. systems where time does not advance
in discrete time steps\, but instead passes continuously\, e.g. as in syst
ems defined by ordinary differential equations). This problem was consider
ed by mathematicians since the 1940s\, who developed several characterizat
ions which\, unfortunately\, do not provide an effective way of checking w
hether a given set is an inductive invariant for a given continuous system
. In the past decade great progress has been made by computer scientists i
n developing the tools for reasoning about continuous systems and powerful
results have been reported which essentially solve the problem of inducti
ve invariant checking algorithmically under some reasonable restrictions o
n the nature 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 outline some fundamental practical limitations inherent in current ap
proaches.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Calum Hughes (University of Manchester)
DTSTART:20240517T100000Z
DTEND:20240517T110000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/15
DESCRIPTION:Title: Models of Martin-Löf Type Theory and Algebraic Model Structu
res\nby Calum Hughes (University of Manchester) as part of University
of Birmingham theoretical computer science seminar\n\nLecture held in Asto
n Webb\, WG12.\n\nAbstract\nKnown models of Martin-Löf Type Theory (MLTT)
include isofibrations in the category of groupoids and Kan fibrations in
the category of simplicial sets. It is an open problem to prove constructi
vely that Kan fibrations model Homotopy Type Theory. One suggested way to
approach this problem is with an algebraic perspective\; the idea being th
at by keeping track of the algebraic data throughout calculations\, proofs
become more constructive. Classically\, normal isofibrations are the alge
bras for the right class of a type theoretic algebraic weak factorisation
system which form part of an algebraic model structure. Constructively\, h
owever\, 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 connecti
on by proving constructively that cloven 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. I will also briefly discu
ss how this result holds more generally\, providing an internal-groupoidal
model of MLTT with links to an algebraic model structure.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sam van Gool (IRIF\, Paris)
DTSTART:20240524T100000Z
DTEND:20240524T110000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/16
DESCRIPTION:Title: Deciding unifiability by folding coalgebras\nby Sam van G
ool (IRIF\, Paris) as part of University of Birmingham theoretical compute
r science seminar\n\nLecture held in Aston Webb\, WG12.\n\nAbstract\nThe u
nifiability problem for a logic L asks to decide whether or not\nthere exi
sts a syntactic substitution that renders two given formulas\nequivalent i
n L.\n\nThe first objective of this talk is to show how the unifiability p
roblem\nfor a logic can often be usefully reformulated as a problem about\
nhomomorphisms between coalgebras.\n\nThe second objective is to showcase
this method in the context of the\ntemporal logic of next\, that is\, clas
sical propositional logic with a\ndeterministic unary modality. In this sp
ecific case\, we show that the\nunifiability problem is equivalent to a ho
momorphism mapping problem for\na sequence of graphs known in the literatu
re as De Bruijn graphs. We\nsolve the homomorphism mapping problem\, emplo
ying methods rooted in\nstring compression\, and thus establishing decidab
ility of unifiability\nfor the temporal logic of next.\n\nThis work is par
t of an ongoing collaboration with Johannes Marti and\nMichelle Sweering.\
n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/16/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ambroise Lafont (École Polytechnique)
DTSTART:20240531T100000Z
DTEND:20240531T110000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/17
DESCRIPTION:Title: A diagram editor to mechanise categorical proofs\nby Ambr
oise Lafont (École Polytechnique) as part of University of Birmingham the
oretical computer science seminar\n\nLecture held in LG23\, Computer Scien
ce.\n\nAbstract\nDiagrammatic proofs are ubiquitous in certain areas of ma
thematics\, especially in category theory. Mechanising such proofs is a te
dious task because proof assistants (such as Coq) are text based. We prese
nt a prototypical diagram editor to make this process easier\, building up
on the vscode extension coq-lsp for the Coq proof assistant and a web appl
ication (https://amblafont.github.io/graph-editor/index.html).\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Paul Taylor (University of Birmingham)
DTSTART:20240426T100000Z
DTEND:20240426T110000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/18
DESCRIPTION:Title: Free algebras for functors\, with not an ordinal in sight
\nby Paul Taylor (University of Birmingham) as part of University of Birmi
ngham theoretical computer science seminar\n\nLecture held in Old Gym\, LG
10.\n\nAbstract\nMartin Escardo challenged me to make Pataraia's fixed poi
nt\ntheorem "predicative". Whilst I have never understood the\nmotivation
for that notion\, I have eliminated one instance\nof impredicativity and
isolated 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 i
ts origins\, and if I were\nto credit one person it would be Joachim Lambe
k.\n\nThe problem breaks into two parts\, one finitary and the\nother infi
nitary. The infinitary part says that the\ncategory of pointed endofuncto
rs of a small category\nwith coequalisers is filtered\, so has a terminal
object\nif the given category has the required filtered colimit.\nThis is
probably widely applicable as an alternative to\ntransfinite methods.\n\nT
he finitary 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 functor\nthat are have a cone over all algebras for it. We\nidentif
y a "special condition" that this construction\nsatisfies and that ensures
that the terminal endofunctor\n(applied to any object) yields the termina
l object of\nthe finitary category\, which is the required initial\nalgebr
a of the functor.\n\nThe hope is that a similar finitary category of\npart
ial models could be found for more complex\nsystems of algebra and logic a
nd that these would\ncorrespond to the intermediate stages in proof\ntheor
etic arguments for normalisation\, cut\nelimination etc.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Wilmer Ricciotti (University of Edinburgh)
DTSTART:20240607T100000Z
DTEND:20240607T110000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/19
DESCRIPTION:Title: Syntactic representation of program execution history\nby
Wilmer Ricciotti (University of Edinburgh) as part of University of Birmi
ngham theoretical computer science seminar\n\nLecture held in LG23\, Compu
ter Science.\n\nAbstract\nAuditing is an increasingly important operation
for computer programming\, for example in security (e.g. to enable history
-based access control) and to enable reproducibility and accountability (e
.g. provenance in scientific programming). Engineering a software system t
o allow history-based auditing by means of ad-hoc instrumentation requires
a substantial effort: the development of general-purpose infrastructure i
s thus very important to achieve the goal of making such techniques widely
available.\n\nInspired by work on Justification Logic\, we study the synt
actic representation of program execution history in the setting of the Ca
lculus of Audited Units\, a core functional language providing auditing as
a first-class operation. CAU automatically materializes execution history
as a data structure and can be implemented by a call-by-value abstract ma
chine in a relatively efficient way. To prove the correctness of our machi
ne\, we extend the language with explicit substitutions and explicit audit
ing operations.\n\nWe discuss applications of auditing by showing how to u
se it to derive various provenance views relating program output to its in
put. Finally\, we present some current work showing a connection between t
he syntactic representation of execution history and the standardisation t
heorem for the lambda calculus.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Stepan Kuznetsov (Steklov Mathematical Insititute)
DTSTART:20240919T100000Z
DTEND:20240919T110000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/21
DESCRIPTION:Title: Substructural logics with Kleene star\nby Stepan Kuznetso
v (Steklov Mathematical Insititute) as part of University of Birmingham th
eoretical computer science seminar\n\nLecture held in Murray UG07.\n\nAbst
ract\nSubstructural 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 sta
r. The basic logic here is so-called action logic\, which extends the mul
tiplicative-additive Lambek calculus. There are two ways of axiomatising t
he Kleene star: a fixpoint one\, yielding action logic\, and a stronger on
e using the omega-rule\, which gives infinitary action logic.\n \nAction l
ogic and infinitary action logic\, both being undecidable\, have different
algorithmic complexity properties. Action logic is finitely axiomatisable
\, thus\, for this logic undecidability means $\\Sigma^0_1$-completeness.
In contrast\, infinitary action logic and its extensions (by finite sets o
f extra axioms and by so-called subexponential modalities) feature a range
of interesting complexity level\, from $\\Pi^0_1$ to $\\Pi^1_1$\, with hy
perarithmetical classes in between.\n \nIn the talk\, we shall give a surv
ey of algorithmic and semantical results for action logic and its variants
. These results include well-known ones by V. Pratt\, D. Kozen\, W. Buszko
wski\, E. Palka\, and others\, as well as recent results obtained by the a
uthor\, solely and in co-authorship with S. Speranski and T. Pshenitsyn.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/21/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Arkadev Chattopadhyay (Tata Institute of Fundamental Research)
DTSTART:20240927T130000Z
DTEND:20240927T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/22
DESCRIPTION:Title: The Power of Randomness in Query and Communication\nby Ar
kadev Chattopadhyay (Tata Institute of Fundamental Research) as part of Un
iversity of Birmingham theoretical computer science seminar\n\nLecture hel
d in LG23\, Computer Science.\n\nAbstract\nHow powerful is randomness for
speeding up algorithms? This is a central question in theoretical computer
science. 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 clo
sely related. In this talk\, I will give a (biased) survey of some of the
intriguing questions that these models raise about the basic nature of ran
domness.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/22/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Christian Konrad (University of Bristol)
DTSTART:20241004T130000Z
DTEND:20241004T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/23
DESCRIPTION:Title: Maximal Matching in Bounded-deletion Streams\nby Christia
n Konrad (University of Bristol) as part of University of Birmingham theor
etical computer science seminar\n\nLecture held in LG23\, Computer Science
.\n\nAbstract\nWe study the Maximal Matching problem in bounded-deletion g
raph streams. In this setting\, a graph $G$ is revealed as an arbitrary se
quence of edge insertions and deletions\, where the number of insertions i
s unrestricted but the number of deletions is guaranteed to be at most $K$
\, for some given parameter $K$. The single-pass streaming space complexit
y of this 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
algorithm and a matching lower bound result that together give a tight und
erstanding (up to poly-log factors) of how the space complexity of Maximal
Matching evolves as a function of the parameter $K$.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/23/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Daniel Gratzer (Aarhus University)
DTSTART:20241018T130000Z
DTEND:20241018T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/24
DESCRIPTION:Title: On synthetic category theory in homotopy type theory\nby
Daniel Gratzer (Aarhus University) as part of University of Birmingham the
oretical computer science seminar\n\nLecture held in LG23\, Computer Scien
ce.\n\nAbstract\nRiehl--Shulman 2017 introduced a version of homotopy type
theory (simplicial type theory or STT) which replaces homotopy type theor
y's slogan that "types are spaces" with the somewhat wordier "some types a
re (∞\,1)-categories". Remarkably\, working in homotopy type theory mean
s that we are able to largely ignore the ∞- part of this slogan\, result
ing in simple proofs of difficult classical results. In this talk we give
an introduction to STT (presupposing only knowledge of type theory and a l
ittle exposure to ordinary categories) and discuss recent work by Gratzer\
, Weinberger\, and Buchholtz on the topic. In particular\, we will focus o
n the construction of a particular type within STT which corresponds to th
e (infinity categorical version of) the category of sets. We shall see tha
t this type can be characterized as a *directed* univalent universe and go
through the first consequences of its addition to STT.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/24/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Giovanni Soldà (Ghent University)
DTSTART:20241108T140000Z
DTEND:20241108T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/25
DESCRIPTION:Title: A proof of Nash-Williams theorem in ATR0\nby Giovanni Sol
dà (Ghent University) as part of University of Birmingham theoretical com
puter science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstr
act\nIn [1]\, Crispin Nash-Williams proved that if (Q\, ≤Q) is a well qu
asi-order (henceforth wqo)\, then so is the set of transfinite sequences o
ver Q with finite range\, ordered by embeddability. In this talk\, we will
show that this result is provable in the subsystem of second-order arithm
etic ATR0: together with previous results by Shore [2]\, this determines t
he reverse mathematical strength of Nash-Williams’ result. In order to d
o this\, we will go via the notion of better quasi-order\, which makes it
possible to develop an equivalence between the iterated powerset of a qo Q
and the iterated powerset over Q. This is joint work with Fedor Pakhomov.
\n\nReferences\n\n[1] C. Nash-Williams\, On well-quasi-ordering transfinit
e sequences\, Mathematical Proceedings of the Cambridge Philosophical Soci
ety 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 sixti
eth birthday\, 1993\, pp. 782–813.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/25/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Luca Reggio (Università degli Studi di Milano)
DTSTART:20241122T140000Z
DTEND:20241122T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/26
DESCRIPTION:Title: Resource-bounded logics: a categorical and modal view\nby
Luca Reggio (Università degli Studi di Milano) as part of University of
Birmingham theoretical computer science seminar\n\nLecture held in LG23\,
Computer Science.\n\nAbstract\nLogics obtained by constraining the availab
le syntactic resources\, such as first-order logic with a finite number of
variables or with bounded quantifier rank\, are central to finite model t
heory and descriptive complexity. I will describe a categorical approach t
o the study of these logic fragments based on so-called game comonads. I w
ill explain how the main properties of the categories of coalgebras for th
ese comonads lead to the axiomatic notion of arboreal categories\, which i
n turn suggests a modal treatment of many resource-bounded logics.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/26/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sebastian Enqvist (Stockholm University)
DTSTART:20241129T140000Z
DTEND:20241129T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/27
DESCRIPTION:Title: Computational content of classical cyclic proofs\nby Seba
stian Enqvist (Stockholm University) as part of University of Birmingham t
heoretical computer science seminar\n\nLecture held in LG23\, Computer Sci
ence.\n\nAbstract\nMuch of the literature on cyclic and non-wellfounded pr
oofs view such proofs from a Curry-Howard or "proofs-as-programs" perspect
ive. Cyclic proofs are natural in this regard as they handle induction by
allowing proofs themselves to be recursively defined\, rather than adding
extra induction axioms or rules. In this talk I will present some early-st
age work on combining this approach with a long-standing theme in proof th
eory\, the computational content of classical proofs. I will begin by givi
ng some background and general thoughts on computational interpretations o
f classical logic. After that I will present a proposal for an approach\,
based on a version of Parigot's lambda-mu-calculus with non-wellfounded te
rms. I will sketch how this calculus can be used to extract computational
content from proofs in classical FOL extended with inductive predicates. I
will also talk about ongoing work to establish some basic properties of t
he calculus\, in particular subject reduction\, confluence and normalizati
on.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/27/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tamio-Vesa Nakajima (University of Oxford)
DTSTART:20241011T130000Z
DTEND:20241011T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/28
DESCRIPTION:Title: Bipartite versus triangle-free subgraphs\nby Tamio-Vesa N
akajima (University of Oxford) as part of University of Birmingham theoret
ical computer science seminar\n\nLecture held in LG23\, Computer Science.\
n\nAbstract\nSuppose we are given a graph G\, which we are promised has a
bipartite subgraph admitting x edges. Can we then find a triangle-free sub
graph admitting a * x edges\, for some approximation ratio a? This talk wi
ll discuss the complexity of this problem for various values of a\, as wel
l as go through connections with other computational problem such as maxim
um cut\, and maximisation versions of PCSPs. As an application\, we will d
iscuss a maximisation version of the Brakensiek-Guruswami conjecture for t
he approximate graph homomorphism problem.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/28/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sky Wilshaw (University of Nottingham)
DTSTART:20241025T130000Z
DTEND:20241025T140000Z
DTSTAMP:20260404T131157Z
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 Bir
mingham theoretical computer science seminar\n\nLecture held in LG23\, Com
puter Science.\n\nAbstract\nIn this talk\, I will discuss the experiences
and challenges of running a successful formalisation project: proving the
consistency of Quine’s set theory New Foundations. The main focus will b
e on the interesting and unexpected ways in which large formalisation proj
ects differ from small ones\, and how we can use formalisation to get bett
er at ‘paper’ mathematics.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/29/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Soumyajit Paul (University of Liverpool)
DTSTART:20241101T140000Z
DTEND:20241101T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/30
DESCRIPTION:Title: Drinking is not good for driving\, nor for computation : comp
lexity of solving games with imperfect information\nby Soumyajit Paul
(University of Liverpool) as part of University of Birmingham theoretical
computer science seminar\n\nLecture held in LG23\, Computer Science.\n\nAb
stract\nIn perfect information games such as Chess and Go\, players observ
e everything. Zermelo\, in his seminal work\, showed that the winner in a
win-lose version of Chess can be determined using backward induction. This
provided a polynomial time algorithm for computing the winner in any perf
ect information game. On the other hand\, in games with imperfect informat
ion such as Bridge and Poker\, players don't observe opponents' hands of c
ards and 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 perfect recall\, i.e. players perfectly remember their past decisions
. These games can be solved in polynomial time. Imperfect recall in genera
l can capture strange situations. Players can even forget if they have enc
ountered the same decision point before\, demonstrated using the game of a
bsentminded driver by Piccione and Rubinstein.\n\nIn this talk\, we will t
ake a tour of the complexity of solving finite games with imperfect inform
ation. We will discuss existing results and also new complexity bounds for
solving imperfect recall games. For new lower bounds\, we relate to probl
ems such as the Square Root Sum problem as well as complexity classes invo
lving computation over reals. More precisely\, we consider the Existentia
l Theory of Reals (ETR) and other fragments of the First Order Theory of R
eals (FOTR). We will also see new tractable classes within imperfect recal
l. This is from joint work with Hugo Gimbert\, B. Srivathsan and Kristoffe
r Arnsfelt Hansen.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/30/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sergey Goncharov (University of Birmingham)
DTSTART:20241115T140000Z
DTEND:20241115T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/31
DESCRIPTION:Title: Introduction to Higher-Order Mathematical Operational Semanti
cs\nby Sergey Goncharov (University of Birmingham) as part of Universi
ty of Birmingham theoretical computer science seminar\n\nLecture held in L
G23\, Computer Science.\n\nAbstract\nReasoning about program equivalence i
n higher-order setting is one of the central topics in computer science\,
with the classical lambda-calculus as a prototypical example and with its
countless flavors and extensions thereof\, all the way up to Haskell and O
Caml. A recently emerged program of higher-order mathematical operational
semantics aims to abstract and unify reasoning methods for such languages
on the basis of two parameters: the language syntax and its (small-step) o
perational semantics. Thus\, higher-order mathematical operational semanti
cs is a natural extension of the pioneering Turi and Plotkin's (first-orde
r) mathematical 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.
Additionally\, I will survey\, more succinctly\, subsequent advances of th
is program\, outline challenges and perspectives for further work.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/31/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Amin Karamlou (Oxford)
DTSTART:20241206T140000Z
DTEND:20241206T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/32
DESCRIPTION:Title: Quantum relaxations of CSP and structure isomorphism\nby
Amin Karamlou (Oxford) as part of University of Birmingham theoretical com
puter science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstr
act\nWe investigate quantum relaxations of two key decision problems in co
mputer science: the constraint satisfaction problem (CSP) and the structur
e isomorphism problem. CSP asks whether a homomorphism exists between two
relational structures\, while structure isomorphism seeks an isomorphism b
etween them. In recent years\, it has become increasingly apparent that ma
ny special cases of CSP can be reformulated in terms of the existence of p
erfect classical strategies in non-local games\, a key topic of study in q
uantum information theory. These games have allowed us to study quantum ad
vantage in relation to many important decision problems\, such as the k-co
louring problem\, and the problem of solving binary constraint systems. Ab
ramsky et al. (2017) have shown that all of these games can be seen as spe
cial instances 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 graded monad on the category of relational structures\, which they dub t
he quantum monad. In this way\, the quantum monad provides a categorical c
haracterisation of quantum advantage for the non-local CSP game.\n\nIn thi
s talk we shall answer several open questions about the non-local CSP game
. We then study a non-local structure isomorphism game\, which generalises
the well-studied graph isomorphism game. We show how the construction of
the quantum monad can be refined to provide categorical semantics for quan
tum strategies in this game. This results in a category where morphisms co
incide with quantum homomorphisms and isomorphisms coincide with quantum i
somorphisms.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/32/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Morgan Rogers (LIPN\, Université Paris 13)
DTSTART:20241213T140000Z
DTEND:20241213T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/33
DESCRIPTION:Title: Topoi with enough points\nby Morgan Rogers (LIPN\, Univer
sité Paris 13) as part of University of Birmingham theoretical computer s
cience seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\njw
w Ivan Di Liberti\, https://arxiv.org/pdf/2403.15338\n\nTo include a wider
audience\, here are two perspectives on the topic of my talk.\n\nGrothend
ieck toposes are sometimes described as generalized spaces\, owing to the
fact that a motivating example is the category of sheaves on a topological
space and many properties of the space are reflected in the categorical s
tructure in a way that can be generalized to other Grothendieck toposes. F
or sufficiently separated spaces (the so-called sober spaces\, notably inc
luding all Hausdorff spaces)\, the construction of the category of sheaves
is even a fully faithful embedding of spaces and continuous maps into the
(2-)category of toposes and geometric morphisms\, and points become geome
tric morphisms Set --> Sh(X). One consequence of this point of view is tha
t one might expect to be able to apply pointwise reasoning to toposes\, to
understand the objects and constructs within a topos by examining what th
ey look like at points. This turns out not to be possible in general! A to
pos is said to have enough points if any pair of distinct morphisms is dis
tinguished by a point.\n\nGrothendieck toposes classify theories in geomet
ric logic\, a fragment of infinitary first-order logic in which only finit
e conjunctions\, set-indexed disjunctions and existential quantification a
re allowed in the construction of formulae (and axioms are sequents assert
ing that one such formula entails another). That a topos E "classifies" su
ch a theory T means that the models of T in any Grothendieck topos F corre
spond to geometric morphisms F --> E. In particular\, set-theoretic models
correspond to morphisms Set --> E\, which is to say points of E. The clas
sifying topos of T having enough points exactly says that T is complete wi
th respect to its set-valued models.\n\nSome sufficient conditions for a t
opos to have enough points emerged fairly early in the development of topo
s theory (Deligne\, Makkai-Reyes)\, but the extent to which they are relat
ed to one another or could be extended was not apparent. In this talk I pr
esent the state of the art\, alongside some examples indicating that impro
ving our results will be tricky!\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/33/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Laura Bocchi (University of Kent)
DTSTART:20250124T140000Z
DTEND:20250124T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/34
DESCRIPTION:Title: Asynchronous Session Subtyping by Trace Relaxation\nby
Laura Bocchi (University of Kent) as part of University of Birmingham theo
retical computer science seminar\n\nLecture held in LG23\, Computer Scienc
e.\n\nAbstract\nSession types are a formalism for modelling structured com
munications in concurrent systems and can be seamlessly implemented into p
rogramming languages. Session subtyping answers the question of whether a
program in a concurrent system can be safely substituted for another\, whe
n their communication behaviours are described by session types. \nAsynchr
onous session subtyping is undecidable in general\, hence the interest in
devising sound (though incomplete) subtyping algorithms. State-of-the-art
methods rely on a data structure known as input trees. I will present an a
lternative approach that replaces input trees with sets of traces\, enabli
ng the application of abstract interpretation techniques to this problem.
This trace-based approach introduces a novel way to relax (enlarge) trace
sets while maintaining observable subtyping properties. Crucially\, these
relaxations can be finitely represented\, even when the corresponding inpu
t trees are arbitrarily large. This method can be instantiated using regul
ar expressions\, enabling us to mechanically prove subtyping for communica
tion patterns previously beyond reach.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/34/
END:VEVENT
BEGIN:VEVENT
SUMMARY:John Sylvester (University of Liverpool)
DTSTART:20250131T140000Z
DTEND:20250131T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/35
DESCRIPTION:Title: Adjacency Labeling Schemes for Small Classes\nby John Syl
vester (University of Liverpool) as part of University of Birmingham theor
etical computer science seminar\n\nLecture held in LG23\, Computer Science
.\n\nAbstract\nAn adjacency labeling scheme for a class of graphs $\\mathc
al{C}$ defines\, for any $n$-vertex $G \\in \\mathcal{C}$\, an assignment
of labels to each vertex in $G$ so that adjacency in $G$ is determined by
a (fixed) function of the two labels of the endpoints. The size of a label
ing scheme is the bit length of the longest label\, which we want as small
as possible. If $|\\mathcal{C}_n|$ denotes the number of $n$-vertex graph
s in $\\mathcal{C}$\, then any adjacency labeling scheme has size at least
$(\\log|C_n|)/n$. \n\nFor many classes (e.g.~planar\, bounded twin-widt
h\, bounded degeneracy) this lower bound is tight. In 1988 the Implicit Gr
aph Conjecture (IGC) postulated that any hereditary (closed under induced
subgraphs) class $\\mathcal{C}$ with $|\\mathcal{C}_n|=2^{O(n\\log n)}$ a
dmits a labeling scheme of size $\\Theta(\\log n)$\, matching the lower bo
und. Hatami & Hatami recently disproved this\, using the probabilistic met
hod to construct a hereditary factorial class requiring almost $\\sqrt{n}$
size labels.\n\nWe begin with a more gentle introduction to labeling sche
mes\, before outlining what we think to be the correct reformulation of th
e 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 (exclude
s some fixed bipartite complete graph as a subgraph). We also prove that t
he conjecture holds if one relaxes the size bound to $O(\\log^3 n)$\, impr
oving on the previously best-known upper bound of $n^{1-\\Omega(1)}$. \n\
nThis is joint work with Édouard Bonnet\, Julien Duron\, Viktor Zamaraev
& Maksim Zhukovskii.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/35/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Daniel Hausmann (University of Liverpool)
DTSTART:20250207T140000Z
DTEND:20250207T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/36
DESCRIPTION:Title: Infinite-duration Games in Formal Methods\nby Daniel Haus
mann (University of Liverpool) as part of University of Birmingham theoret
ical computer science seminar\n\nLecture held in LG23\, Computer Science.\
n\nAbstract\nInfinite duration two-player games have been established as a
formalism for the treatment of decision problems for various temporal log
ics. Such games can be used to evaluate qualitative temporal properties\,
subsuming safety\, reachability\, or general liveness properties\, which a
re typically given in the form of omega-regular winning conditions.\n\nThi
s talk will first give an overview on how omega-regular games are used as
a central back-end tool for reactive synthesis (LTL synthesis)\, and for m
odel and satisfiability checking for fixpoint logics (such as the modal mu
-calculus).\n\nSubsequently\, the talk will present recent progress regard
ing algorithms for the analysis of two types of omega-regular games: Emers
on-Lei games and obliging games. In the former\, the winning condition is
an arbitrary Boolean combination of events that should occur infinitely of
ten (or only finitely often). The latter encode a certain degree of cooper
ation between the two players.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/36/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Matthew Alan Le Brun (University of Glasgow)
DTSTART:20250228T140000Z
DTEND:20250228T150000Z
DTSTAMP:20260404T131157Z
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 theoreti
cal computer science seminar\n\nLecture held in LG23\, Computer Science.\n
\nAbstract\nTypes in programming languages abstract away the specifics of
a program to provide a lightweight form of static verification. Multiparty
Session Types (MPST) do just that for message passing programs where many
participants communicate together via a multiparty session. Traditionally
\, recursion has been the preferred method of describing infinite computat
ion in MPST\; in this study\, we investigate the use of replication\, an a
lternative construct to recursion that denotes a process as one which is i
nfinitely available. We introduce MPST!\, a session-typed multiparty proce
ss calculus with replication and first-class roles. We find that replicati
on is not an equivalent alternative to recursion in MPST\, and using both
constructs in one type system in fact allows us to express both context-fr
ee protocols and protocols that make interesting use of mutual exclusion a
nd races. In this talk\, we will demonstrate the expressiveness of replica
tion in MPST by example\, observe the mutual non-inclusion result\, and di
scuss the decidability of typechecking.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/37/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rodrigo Nicolau Almeida (ILLC\, University of Amsterdam)
DTSTART:20250404T130000Z
DTEND:20250404T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/39
DESCRIPTION:Title: Heyting algebras one step at a time\nby Rodrigo Nicolau A
lmeida (ILLC\, University of Amsterdam) as part of University of Birmingha
m theoretical 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
propositional calculus\, IPC\, as well as in connection with point-free t
opology and the lambda calculus\, where they appear naturally. A lot of th
is work has been assisted by Esakia duality\, which represents such algebr
as using ordered-topological spaces with a particular structure. Despite t
his intense work\, several basic questions concerning (1) constructions of
Heyting algebras - especially concerning free algebras\, coproducts and o
ther initial-like constructions have remained unanswered or been left outs
ide 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 an
d related structures\, as well as highlight its potential use in attacking
some open questions in the study of extensions of intuitionistic logic:\n
\nKuznetsov's problem: whether every variety of Heyting algebras is genera
ted by its complete algebras.\nPitts and Pataraia’s problem: whether eve
ry Heyting 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://stable.researchseminars.org/talk/TheoryCSBham/39/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rini Banerjee (University of Cambridge)
DTSTART:20250214T140000Z
DTEND:20250214T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/40
DESCRIPTION:Title: Fulminate: Testing CN Separation-Logic Specifications in C\nby Rini Banerjee (University of Cambridge) as part of University of Bir
mingham theoretical computer science seminar\n\nLecture held in LG23\, Com
puter Science.\n\nAbstract\nSystems code (e.g. operating systems\, hypervi
sors) forms a crucial part of our everyday computing infrastructure\, with
much of it written in C/C++. Virtually all C/C++ programs involve manual
memory management via pointers\, leading to complex ownership patterns tha
t are difficult to describe formally. Separation logic has become an impo
rtant tool for capturing and reasoning about these ownership patterns\, fo
rming the basis of several static analysis and proof tools (e.g. CN [1]\,
a verification tool for C). However\, little work has been done on testing
separation logic specifications in concrete execution\, since at first gl
ance\, separation-logic formulas are hard to evaluate in a reasonable amou
nt of time. In this talk I describe our work on Fulminate [2]\, a tool for
testing CN separation-logic specifications on concrete inputs in C.\n\n[1
] CN: Verifying Systems C Code with Separation-Logic Refinement Types. Chr
istopher Pulte\, Dhruv C. Makwana\, Thomas Sewell\, Kayvan Memarian\, Pete
r Sewell\, Neel Krishnaswami. POPL 2023.\n[2] Fulminate: Testing CN Separa
tion-Logic Specifications in C. Rini Banerjee\, Kayvan Memarian\, Dhruv Ma
kwana\, Christopher Pulte\, Neel Krishnaswami\, Peter Sewell. POPL 2025.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/40/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Karteek Sreenivasaiah (University of Liverpool)
DTSTART:20250221T140000Z
DTEND:20250221T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/41
DESCRIPTION:Title: Unconditional lower bounds for Orthogonal Vectors\nby Kar
teek Sreenivasaiah (University of Liverpool) as part of University of Birm
ingham theoretical computer science seminar\n\nLecture held in LG23\, Comp
uter Science.\n\nAbstract\nFine-grained complexity is a modern area of com
puter science that has been successful in identifying problems that are bo
ttlnecks to computation within finer levels of polynomial time. One such f
unction is Orthogonal Vectors (OV) -- given two tuples A and B of n Boolea
n vectors\, each of dimension d\, decide if there exists a vector in A and
a vector in B such that they are othogonal.\n\nIt has been established th
at several important functions have faster algorithms only if OV does. In
very informal terms\, an instance of OV is hiding inside these functions.
Hence computing these functions essentially involves computing the OV inst
ance embedded inside them. \n\nA central conjecture in fine-grained comple
xity known 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 th
e OV conjecture for a restricted model of depth-3 Boolean circuits. The fo
cus of the talk is on the combinatorial ideas that are used to show such a
n unconditional lower bound. No background in circuits or fine-grained com
plexity is assumed.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/41/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Caterina Viola (University of Catania)
DTSTART:20250321T140000Z
DTEND:20250321T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/42
DESCRIPTION:Title: Algebraic Approach to Approximation\nby Caterina Viola (U
niversity of Catania) as part of University of Birmingham theoretical comp
uter science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstra
ct\nWhat makes a computational problem easy or hard to solve approximately
? In this talk\, we introduce valued promise CSPs (valued PCSPs)\, a broad
class that includes CSPs\, valued CSPs\, and various approximation proble
ms. We present the key algebraic structures that capture their complexity
and enable polynomial-time reductions. Using illustrative examples\, we sh
ow how this framework unifies known results and offers new insights into c
omputational hardness.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/42/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Mario Román (University of Oxford)
DTSTART:20250307T140000Z
DTEND:20250307T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/43
DESCRIPTION:Title: String Diagrams for Premonoidal Categories\nby Mario Rom
án (University of Oxford) as part of University of Birmingham theoretical
computer science seminar\n\nLecture held in LG23\, Computer Science.\n\nA
bstract\nPremonoidal categories are monoidal categories without the interc
hange law while effectful categories are premonoidal categories with a cho
sen monoidal subcategory of interchanging morphisms. In the same sense tha
t string diagrams\, pioneered by Joyal and Street\, are an internal langua
ge for monoidal categories\, we will see how string diagrams with an added
"runtime object"\, pioneered by Alan Jeffrey\, are an internal language f
or effectful categories and can be used as string diagrams for effectful\,
premonoidal\, and Freyd categories. This talk is partly based on joint wo
rk with Paweł Sobociński.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/43/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Vincent Moreau (IRIF\, Paris)
DTSTART:20250328T140000Z
DTEND:20250328T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/44
DESCRIPTION:Title: Profinite lambda-terms and higher-order regular languages
\nby Vincent Moreau (IRIF\, Paris) as part of University of Birmingham the
oretical computer science seminar\n\nLecture held in LG23\, Computer Scien
ce.\n\nAbstract\nFor several years now\, there has been a growing connecti
on between automata theory and λ-calculus\, in terms of syntax\, semantic
s and logic. The notion of language of λ-terms recognized by a cartesian
closed category\, introduced by Salvati\, is a fundamental contribution to
this convergence as it generalizes to the higher-order the usual regular
language 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 recognize exactly these languages. To achieve this\, we establish a cl
ose link with the implicit automata programme of Nguyen and Pradic. Second
\, we explain how higher-order regular languages assemble into a fibration
and what this means in terms of quantifiers in the style of MSO. Third\,
we introduce profinite λ-terms\, a higher-order generalization of the not
ion of profinite word related to regular languages by Stone duality. These
assemble into a cartesian closed category which verifies an adequate univ
ersal property with respect to finite models\, justifying the denomination
of profinite λ-calculus.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/44/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Geoff Sutcliffe (University of Miami)
DTSTART:20250509T130000Z
DTEND:20250509T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/45
DESCRIPTION:Title: The TPTP World - Infrastructure for Automated Reasoning\n
by Geoff Sutcliffe (University of Miami) as part of University of Birmingh
am theoretical computer science seminar\n\nLecture held in LG23\, Computer
Science.\n\nAbstract\nThe TPTP World is the established infrastructure us
ed by the Automated Theorem Proving (ATP) community for research\, develop
ment\, and deployment of ATP systems. The data\, standards\, and services
provided by the TPTP World have made it easy to develop\, evaluate\, and d
eploy ATP technology. This talk and tutorial reviews the core features of
the TPTP World\, describes key services of the TPTP World\, and presents s
ome successful applications. The use of ATP as the reliable substrate to s
ubsymbolic AI systems (e.g.\, LLMs)\, to form neurosymbolic AI systems\, i
s reviewed.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/45/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rahaleh Jalali (University of Bath)
DTSTART:20250516T130000Z
DTEND:20250516T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/46
DESCRIPTION:Title: Skolemization and the logic of quantifier shifts\nby Raha
leh Jalali (University of Bath) as part of University of Birmingham theore
tical computer science seminar\n\nLecture held in LG23\, Computer Science.
\n\nAbstract\nSkolemization is a method to remove strong quantifiers (i.e.
\, positive occurrences of the universal quantifier and negative occurrenc
es of the existential quantifier) from a first-order formula and replace t
hem with fresh function symbols. It is a well-known fact that Skolemizatio
n is sound and complete with respect to the classical predicate logic\, CQ
C. At the same time\, this is not the case for the intuitionistic predicat
e logic\, IQC. In this talk\, we consider the three formulas known as the
"quantifier shifts"\, which are provable in CQC but not in IQC. One may su
spect that the failure of the quantifier shifts is why Skolemization fails
in IQC. Therefore\, asking what happens if we add the quantifier shifts t
o IQC is natural. Does the resulting logic have Skolemization? If not\, fo
r which class of formulas does the Skolemization hold? These questions bui
ld the motivation of the present research study that investigates the logi
c of quantifier shifts and its Skolemization. This is a joint work with Ma
tthias Baaz\, Rosalie Iemhoff\, and Mariami Gamsakhurdia.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/46/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sayan Bhattacharya (University of Warwick)
DTSTART:20250523T130000Z
DTEND:20250523T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/47
DESCRIPTION:Title: Vizing's Theorem in Near-Linear Time\nby Sayan Bhattachar
ya (University of Warwick) as part of University of Birmingham theoretical
computer science seminar\n\nLecture held in LG23\, Computer Science.\n\nA
bstract\nA textbook theorem by Vizing from the 1960s guarantees that any g
raph with n nodes\, m edges and maximum degree \\Delta admits a proper edg
e coloring 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 n
ear-linear time algorithm for this fundamental problem. Our algorithm runs
in only O(m \\log \\Delta) time\; this matches the longstanding O(m \\log
\\Delta) time bound for computing a \\Delta-edge coloring in bipartite gr
aphs.\n\nJoint work with Sepehr Assadi\, Soheil Behnezhad\, Martin Costa\,
Shay Solomon and Tinayi Zhang.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/47/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dylan McDermott (University of Oxford)
DTSTART:20250530T130000Z
DTEND:20250530T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/48
DESCRIPTION:Title: Notions of presentation for graded monads\nby Dylan McDer
mott (University of Oxford) as part of University of Birmingham theoretica
l computer science seminar\n\nLecture held in LG23\, Computer Science.\n\n
Abstract\nMonads\, and their presentations through operations and equation
s\, are used to model computations involving effects\, such as mutable sta
te and nondeterministic choice. When we want to track information about th
e effects of computations\, for instance in a type-and-effect analysis\, w
e instead 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 graded presentation that appears naturally when we think about what ki
nd of graded algebraic structures correspond to graded monads\, and these
graded presentations satisfy analgous properties to those we get in the un
graded setting. Unfortunately\, it turns out they don't work very well for
effects of interest. I will therefore introduce a more general notion of
_flexibly_ graded presentation\, one that better captures the effects. To
do this we have to depart slightly from the usual techniques for doing alg
ebraic theories\, but I will argue that we do not lose too much by doing s
o.\n\nThis talk is based on joint work with Shin-ya Katsumata\, Tarmo Uust
alu\, and Nicolas Wu\, described in the following papers:\n Dylan McDermo
tt and Tarmo Uustalu\, Flexibly graded monads and graded algebras\, MPC 20
22\n Shin-ya Katsumata\, Dylan McDermott\, Tarmo Uustalu and Nicolas Wu\,
Flexible presentations of graded monads\, ICFP 2022\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/48/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nikhil Mande (University of Liverpool)
DTSTART:20250606T130000Z
DTEND:20250606T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/49
DESCRIPTION:Title: On Kings in Tournaments\nby Nikhil Mande (University of L
iverpool) as part of University of Birmingham theoretical computer science
seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nA tourna
ment is a complete directed graph. These graphs model round-robin tourname
nts such as the premier league. A king in a tournament is a vertex k such
that every other vertex is reachable by a path of length 1 or 2 from k. It
is well known that every tournament has a king\, in particular a maximum
out-degree vertex is a king. I will talk about my recent results on the co
mplexity of finding a king\, and other variants of winners\, in a tourname
nt. No technical background will be assumed.\nBased on joint works with Zi
ad Ismaili Alaoui\, Manaswi Paraashar\, Swagato Sanyal\, and Nitin Saurabh
.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/49/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Parinya Chalermsook (University of Sheffield)
DTSTART:20250620T130000Z
DTEND:20250620T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/50
DESCRIPTION:Title: Extremal Combinatorics Meets Algorithms and Data Structures\nby Parinya Chalermsook (University of Sheffield) as part of University
of Birmingham theoretical computer science seminar\n\nLecture held in Ast
on Webb Dome Lecture Theatre.\n\nAbstract\nThis talk explores a rich inter
play between extremal combinatorics and the analysis of algorithms and dat
a structures. In the first part of the talk\, I will explain how classical
Ramsey theory tightly captures a fundamental question in approximation al
gorithms and how the LP rounding perspectives (techniques that are central
in approximation algorithms) led to breaking a 6-decade-old extremal boun
d on rectangle coloring. In the second part\, I will discuss the role of e
xtremal combinatorics in the context of sorting and binary search trees (i
n particular\, the long-standing dynamic optimality conjecture). In both s
cenarios\, such interplay has been crucial in making progress and highligh
ts the two-way dialogue between the two fields.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/50/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Guillaume Munch-Maccagnoni (INRIA Nantes)
DTSTART:20250627T130000Z
DTEND:20250627T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/51
DESCRIPTION:Title: Resource management in programming\, call-by-push-value\, and
ordered logic\nby Guillaume Munch-Maccagnoni (INRIA Nantes) as part o
f University of Birmingham theoretical computer science seminar\n\nLecture
held in LG23\, Computer Science.\n\nAbstract\nAlthough linear logic was s
een as a source of inspiration for the design of programming languages (pr
omising to reconcile imperative and functional programming to some\, no le
ss!)\, the integration of notions of linearity in programming language the
ory has been slow. Examples are rarer to come by than meaningful models of
effectful computation determined by monads\, as are examples that meaning
fully mix linearity and effects. We propose a new example (which meaningfu
lly refines linear logic\, and meaningfully mixes linearity and effects) w
hose motivation is to model the notion of resource from the C++ and Rust p
rogramming languages. In these languages\, a resource is a value abstracti
on for some state which requires that some clean-up action is correctly pe
rformed at a specific moment. These languages show a possible (and in prac
tice widely successful) way to integrate resources with control (e.g. exce
ptions). Similarly\, our model shows how linearity can be combined with co
ntrol effects such as the exception monad\, exhibiting similar features as
C++/Rust. The main tool we use is the decomposition of notions of computa
tion into adjunctions provided by call-by-push-value (CBPV). Somehow\, thi
s endeavour requires us to refine the notion of linear CBPV model into an
ordered (i.e. non-commutative) CBPV.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/51/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Antonio Lorenzin (UCL)
DTSTART:20250926T130000Z
DTEND:20250926T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/53
DESCRIPTION:Title: Categories of abstract and noncommutative measurable spaces\nby Antonio Lorenzin (UCL) as part of University of Birmingham theoreti
cal computer science seminar\n\nLecture held in LG23\, Computer Science.\n
\nAbstract\nIn quantum probability\, the category of $C^*$-algebras and co
mpletely positive unital (cpu) maps is a well-established setting. However
\, its classical side\, given by commutative $C^*$-algebras\, does not con
tain all regular conditional probabilities\, a central concept in classica
l probability. This shortcoming is due to the inherent topological nature
of $C^*$-algebras\, which ties them to continuous rather than measurable s
tructures.\n\nTo address this\, we investigate what noncommutative (or qua
ntum) measurable spaces should be\, by establishing adjunctions and equiva
lences between special classes of $C^*$-algebras and cpu maps and categori
es of measurable spaces and Markov kernels. On the classical side\, these
can be equivalently described by Boolean σ-algebras (also known as abstra
ct measurable spaces). Moreover\, our operator-algebraic analysis equips t
hese structures with a generalized notion of Markov kernels\, realized as
POVMs. \n\nUltimately\, we obtain a categorical framework in which both cl
assical and quantum probability coexist\, and the classical side has regul
ar conditional probabilities.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/53/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nachi Valliappan (University of Edinburgh)
DTSTART:20251003T130000Z
DTEND:20251003T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/54
DESCRIPTION:Title: Lax modal lambda calculi\nby Nachi Valliappan (University
of Edinburgh) as part of University of Birmingham theoretical computer sc
ience seminar\n\nLecture held in LC-UG10 Murray Learning Centre.\n\nAbstra
ct\nIntuitionistic modal logic (IML) is the study of extending intuitionis
tic propositional logic with modal operators such as the box and diamond m
odalities. Advances in IML have led to a plethora of useful applications i
n programming languages via the development of corresponding type theories
with modalities. Until recently\, IMLs with diamonds had been misundersto
od as somewhat peculiar and unstable\, causing the development of type the
ories with diamonds to lag behind type theories with boxes.\n\nIn this tal
k\, I will present a family of typed-lambda calculi corresponding to sublo
gics of a peculiar IML with diamonds known as Lax logic. These calculi pro
vide a modal logical foundation for strong functors in functional programm
ing and make it possible to formalize the connection between possible-worl
d semantics for IMLs and categorical semantics for corresponding lambda ca
lculi. I hope to end this talk with a summary of what I’ve learnt from I
ML literature and how it has inspired me to think about semantics of modal
ities in programming languages beyond boxes and diamonds. \n\nA draft arti
cle on this topic can be found here: $\\url{https://nachivpn.me/lmlc.pdf}$
\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/54/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jim de Groot (University of Bern)
DTSTART:20251017T130000Z
DTEND:20251017T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/55
DESCRIPTION:Title: Intuitionistic monotone modal logic\nby Jim de Groot (Uni
versity of Bern) as part of University of Birmingham theoretical computer
science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nW
e introduce 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 intuition
istic neighbourhood models\, which are models whose neighbourhoods can cha
nge when moving along the intuitionistic accessibility relation. We compar
e the resulting logic with other intuitionistic monotone modal logics to f
ind conservativity results resembling those of the logics between CK and I
K.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/55/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ohad Kammar (University of Edinburgh)
DTSTART:20251024T130000Z
DTEND:20251024T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/56
DESCRIPTION:Title: Modular abstract syntax trees (MAST) – substitution tensors
with second-class sorts\nby Ohad Kammar (University of Edinburgh) as
part of University of Birmingham theoretical computer science seminar\n\nL
ecture held in LG23\, Computer Science.\n\nAbstract\nWe adapt Fiore\, Plot
kin\, and Turi's treatment of abstract syntax with binding\, substitution\
, and holes to account for languages with second-class sorts. These situat
ions include programming calculi such as the Call-by-Value λ-calculus (CB
V) and Levy's Call-by-Push-Value (CBPV). Prohibiting second-class sorts fr
om appearing in variable contexts means the presheaf of variables is no lo
nger a left-unit for Fiore et al's substitution tensor product. We general
ised their development to associative and right-unital skew monoidal categ
ories. We reuse much of the development through skew bicategorical argumen
ts. In ongoing work\, we replace the skew monoidal structure with ordinary
monoidal structure by recourse to substitution modules instead of substit
ution monoids.\n\nWe apply the resulting theory in two scenarios. We emplo
y the mathematical theory to circumvent the expression problem when provin
g substitution lemmata for varieties of CBV denotational semantics modular
ly. We employ a computational implementation of the theory to circumvent t
he expression problem when implementing intrinsically-typed foreign-functi
on interfaces for the 29 theories of SMTLIB.\n\nJoint work with Marcelo Fi
ore\, Kajetan Granops\, Mihail-Codrin Iftode\, Georg Moser\, and Sam Stato
n.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/56/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bruno Cavalar (University of Oxford)
DTSTART:20251031T140000Z
DTEND:20251031T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/57
DESCRIPTION:Title: Monotone Circuit Complexity of Matching\nby Bruno Cavalar
(University of Oxford) as part of University of Birmingham theoretical co
mputer science seminar\n\nLecture held in Aston Webb G33.\n\nAbstract\nWe
show that the perfect matching function on n-vertex graphs requires monoto
ne circuits of exponential size. This improves on the quasipolynomial lowe
r bound of Razborov (1985). Our proof uses the standard approximation meth
od together with a new sunflower lemma for matchings.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/57/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Matteo Acclavio (University of Sussex)
DTSTART:20251107T140000Z
DTEND:20251107T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/58
DESCRIPTION:Title: Dealing with Concurrency in Dynamic Logic\nby Matteo Accl
avio (University of Sussex) as part of University of Birmingham theoretica
l computer science seminar\n\nLecture held in LG23\, Computer Science.\n\n
Abstract\nDynamic logic is a versatile framework for reasoning about prope
rties of programs. It extends classical logic with modalities quantifying
propositions based on program executions. In this context\, dealing with c
oncurrency has proved problematic\, mainly because of the difficulty of ca
pturing interleaving. In recent work\, we developed a new framework we cal
l operational propositional dynamic logic (OPDL). The key feature of our a
pproach is to consider programs and their operational semantics as a param
eter of the logic\, allowing us to overcome some limitations of traditiona
l propositional dynamic logic (PDL).\n\nIn this talk\, I will give motivat
ions for this work\, and I will explain the technical aspects of proof of
adequacy –relying on a proof of cut-elimination for a finitely branching
non-wellfounded sequent calculus for PDL. After discussing how traditiona
l PDL can be seen as specific instance of OPDL\, I will show two represent
ative cases of concurrent programming languages: the Calculus of Communica
ting Systems (CCS)\, where concurrency arises from parallel composition\,
and Choreographic Programming\, where it arises from out-of-order executio
n.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/58/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Anupam Das (University of Birmingham)
DTSTART:20251128T140000Z
DTEND:20251128T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/59
DESCRIPTION:Title: Right-linear structures: decomposing the theory of (omega-)re
gular languages via fixed points\nby Anupam Das (University of Birming
ham) as part of University of Birmingham theoretical computer science semi
nar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nIn the second
half of the 20th century various theories of regular expressions were pro
posed\, eventually leading to the notion of a Kleene Algebra (KA). Kozen a
nd Krob independently proved the completeness of KA for the model of regul
ar languages\, a now celebrated result that has been refined and generalis
ed over the years. In recent years proof theoretic approaches to regular l
anguages have been studied\, providing alternative routes to metalogical r
esults like completeness and decidability.\n\nIn this talk I will present
a new approach from a different starting point: finite state automata. A n
otation for non-deterministic finite automata is readily obtained via expr
essions with least fixed points\, leading to a theory of right-linear alge
bras (RLA). RLA is strictly more general than KA\, e.g. admitting ω-regul
ar languages as a model too\, and enjoys a simpler proof theory than KA. T
his allows us to recover (more general) metalogical results in a robust wa
y\, combining techniques from automata\, games\, and cyclic proofs. In par
ticular\, our development exposes a novel factorisation of the completenes
s for KA\, controlling the use of multiplication.\n\nThis talk is based on
several joint works with Abhishek De.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/59/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tikhon Pshenitsyn (Steklov Mathematical Institute)
DTSTART:20251010T130000Z
DTEND:20251010T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/60
DESCRIPTION:Title: First-order linear logic and graph languages\nby Tikhon P
shenitsyn (Steklov Mathematical Institute) as part of University of Birmin
gham theoretical computer science seminar\n\nLecture held in LG23\, Comput
er Science.\n\nAbstract\nLinear logic provides a way of reasoning about re
sources or actions. One of its prominent applications is in linguistics: w
ords and word collocations can be regarded as resources that are combined
into sentences according to certain composition rules. The Lambek calculus
—also known as noncommutative multiplicative intuitionistic linear logic
—serves this purpose by enabling one to generate formal languages. Pentu
s (1993) proved that grammars based on the Lambek calculus generate exactl
y context-free languages. Later\, Pentus (1995) showed that the Lambek cal
culus is sound and complete with respect to formal language models. These
results establish a strong connection between linear logic and the formal
language theory.\n\nThis talk begins with an introduction to linear logic
and the Lambek calculus. After that we turn to discussion of first-order l
inear logic and its recently established connection to the formal language
theory. It turns out that first-order linear logic can be used to generat
e graph languages in the same way the Lambek calculus is used to generate
string languages. Graph grammars based on first-order linear logic generat
e a wider class of languages than graph context-free languages\; the forme
r is closed under intersection and it subsumes linear-time graph transform
ation systems. In the final part of the talk\, we briefly discuss model-th
eoretic aspects of first-order linear logic\, showing that its negative fr
agment is sound and complete w.r.t. graph language semantics.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/60/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Thomas Sauerwald (University of Cambridge)
DTSTART:20251003T143000Z
DTEND:20251003T153000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/61
DESCRIPTION:Title: Balanced Allocations: The Power of Choice versus Noise\nb
y Thomas Sauerwald (University of Cambridge) as part of University of Birm
ingham theoretical computer science seminar\n\nLecture held in Watson Lect
ure Theatre B.\n\nAbstract\nIn the balanced allocation problem we wish to
allocate m balls (jobs) into n bins (servers) by allowing each ball to cho
ose from some bins sampled uniformly at random. The goal is to maintain a
small gap between the maximum load and average load. For the one-choice pr
otocol\, where each ball is allocated to a random bin\, the gap diverges f
or large m. However\, for the two-choice protocol\, where each ball sample
s two bins and is placed in the least loaded of the two\, it was shown mor
e than 20 years ago that the gap is only O(log log n) for all m. This dram
atic improvement is widely known as ``power of two choices’’\, and sim
ilar effects have been observed in hashing and routing.\n\nIn this talk\,
we will present new results in settings where the load information is rest
ricted 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
performance.\n\nThis is based on joint works with Dimitrios Los and John
Sylvester. More information and some illustrations of the results are also
available under:\n\n$\\url{dimitrioslos.com/research/phd-thesis/index.htm
l}$\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/61/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Paul Taylor (University of Birmingham)
DTSTART:20251121T140000Z
DTEND:20251121T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/62
DESCRIPTION:Title: A Categorical Replacement for Replacement\nby Paul Taylor
(University of Birmingham) as part of University of Birmingham theoretica
l computer science seminar\n\nLecture held in LG23\, Computer Science.\n\n
Abstract\nIt is more than 50 years since Lawvere and Tierney introduced el
ementary toposes as an alternative to (bounded) Zermelo set theory and sin
ce then the bulk of mainstream mathematics has been formulated in it. Howe
ver\, there are some constructions such as iterated functors and gluing th
at go outside this framework\, but can be justified using the Axiom-Scheme
of Replacement. Replacement is interesting because it can build skyscrape
rs from plans on the ground\, whereas using universes or large cardinals i
s like dropping building materials from a satellite.\n\nIt is embarrassing
after all this time that category theory does not have a way of expressin
g Replacement in its native language.\n\nIt is a well established and powe
rful discipline that is being applied to more and more subjects. It can st
and 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 n
ot yet been shown to be inconsistent.\n\nThe native language of category t
heory is adjunctions\, which are formally equivalent to introduction--elim
ination rule-sets in type theory: we create a new connective by asserting
that some previously defined functor has an adjoint. The powerful cases ar
e when the adjoint must be defined recursively\, which raises questions of
termination.\n\nTo handle this we use an idea from set theory\, but abstr
acted and generalised using category theory. The proposal is that any well
founded structure have an extensional reflection\, where relations become
coalgebras for fairly general functors and subsets become factorisation s
ystems.\n\nCategorical applications of this such as transfinite iteration
of functors will be considered on a later occasion. In this lecture I will
discuss 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://stable.researchseminars.org/talk/TheoryCSBham/62/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Martin Costa (University of Warwick)
DTSTART:20251114T140000Z
DTEND:20251114T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/63
DESCRIPTION:Title: Nibbling at Long Cycles: Dynamic (and Static) Edge Coloring i
n Optimal Time\nby Martin Costa (University of Warwick) as part of Uni
versity of Birmingham theoretical computer science seminar\n\nLecture held
in LG23\, Computer Science.\n\nAbstract\nWe consider the problem of maint
aining a (1 + ε)Δ-edge coloring in a dynamic graph G with n nodes and ma
ximum degree at most Δ. The state-of-the-art update time is Oε (polylog(
n))\, by Duan\, He and Zhang [SODA'19] and by Christiansen [STOC'23].\n\nT
he following natural question arises: What is the best possible update tim
e of an algorithm for this task? More specifically\, can we bring it all t
he way down to some constant (for constant ε)? This question coincides wi
th the static time barrier for the problem: Even for (2Δ -1)-coloring\, t
here is only a naïve O(m log Δ)-time algorithm.\n\nWe answer this fundam
ental question in the affirmative\, by presenting a dynamic (1 + ε)Δ-edg
e coloring algorithm with poly(1/ε) update time\, provided Δ = Omegaε (
polylog(n)). As a corollary\, we also get the first linear time (for const
ant ε) static algorithm for (1 + ε)Δ-edge coloring\; in particular\, we
achieve a running time of O(m poly(1/ε)).\n\nWe obtain our results by ca
refully combining a variant of the Nibble algorithm from Bhattacharya\, Gr
andoni and Wajc [SODA'21] with the subsampling technique of Kulkarni\, Liu
\, Sah\, Sawhney and Tarnawski [STOC'22].\n\nThis talk is based on joint w
ork with Sayan Bhattacharya\, Nadav Panski and Shay Solomon.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/63/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dimitrios Economou (University of Cambridge)
DTSTART:20251205T140000Z
DTEND:20251205T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/64
DESCRIPTION:Title: Focusing is CBPV but CBPV is almost focusing\nby Dimitrio
s Economou (University of Cambridge) as part of University of Birmingham t
heoretical computer science seminar\n\nLecture held in LG23\, Computer Sci
ence.\n\nAbstract\nHistorically\, focusing arose from the study of proof s
earch in linear logic. Call-By-Push-Value (CBPV) instead arose from the st
udy of computational effects in programming languages. Each of these calcu
li introduces a notion of duality: between left and right inversion (posit
ive and negative formulas) for focused sequent calculi\, and between call-
by-value and call-by-name (value and computation types) for CBPV. Remarkab
ly\, the polarised type structure of these two calculi is absolutely ident
ical. However\, their judgmental structures are quite different\, with foc
using having typing contexts of negative (computation) types which is the
opposite of CBPV’s contexts of value (positive) types. Researchers have
puzzled over their relationship for decades. In this talk\, we clarify the
relationship. \n\nWe recall standard calculi for intuitionistic focusing
and CBPV\, and give categorical semantics for both. We also give syntactic
translations back and forth. We show that the translation from focusing t
o CBPV preserves the denotations of terms exactly\, but that the backwards
translation introduces double polarity shifts that break focusing. Howeve
r\, using a logical relation\, we show that the translation from CBPV to f
ocusing is adequate.\n\nThis is joint work with Neel Krishnaswami.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/64/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alyssa Renata (Imperial College London)
DTSTART:20251212T140000Z
DTEND:20251212T150000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/65
DESCRIPTION:Title: Stone Duality for Monads\nby Alyssa Renata (Imperial Coll
ege London) as part of University of Birmingham theoretical computer scien
ce seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nIn com
puter science\, monads are often interpreted as representing computation w
hich interact with some resource or environment. To what extent can we int
erpret arbitrary monads in this way?\n\nTo answer this question\, I will a
ssociate to each monad its topological behaviour category\, whose objects
are understood as states of the environment\, and whose morphisms are tran
sitions along states. I will also explain how to recover a monad from a to
pological category\, giving rise to an adjunction between the category of
monads on set and a category of topological categories.\n\nWe interpret th
is 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 Stone spectrum\, and the only morphisms are identity. If time permits
\, I will also explain the relationship between our behaviour category and
the Zariski spectrum of commutative rings\, using an abstract framework o
f spectra invented by Diers and Cole.\n\nThis is joint work with Richard G
arner.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/65/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sandra Kiefer (Oxford)
DTSTART:20260130T130000Z
DTEND:20260130T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/66
DESCRIPTION:Title: Long-Refinement Graphs\nby Sandra Kiefer (Oxford) as part
of University of Birmingham theoretical computer science seminar\n\nLectu
re held in LG23\, Computer Science.\n\nAbstract\nThe Colour Refinement alg
orithm is a classical procedure to detect symmetries in graphs\, whose mos
t prominent application is in graph-isomorphism tests. The algorithm evalu
ates local information to compute a colouring for the vertices in an itera
tive fashion. \n\nThe number of iterations that the algorithm takes to ter
minate is its central complexity parameter. For a long time\, it was an op
en question whether graphs that take the maximum theoretically possible nu
mber of Colour Refinement iterations actually exist. My talk will give an
overview 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
infinite families of such long-refinement graphs with degrees 2 and 3\, th
ereby showing that the trivial upper bound on the iteration number of Colo
ur Refinement is tight. Recently\, via reverse-engineering\, T. Devini de
Mel and I obtained a complete characterisation of the long-refinement grap
hs with small (or\, equivalently\, large) degrees. This yields that that\,
with one exception\, the aforementioned families are the only long-refine
ment graphs with maximum degree at most 3\, and hence that all long-refine
ment graphs 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
-refinement graphs that are only distinguished in the last iteration of Co
lour Refinement before termination. In the talk\, I will present a simple
argument to show that such graphs do not exist.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/66/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Fernando Lucatelli Nunes (Birmingham)
DTSTART:20260123T130000Z
DTEND:20260123T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/67
DESCRIPTION:Title: Eilenberg–Moore\, Kleisli and Descent Factorizations\nb
y Fernando Lucatelli Nunes (Birmingham) as part of University of Birmingha
m theoretical computer science seminar\n\nLecture held in LG23\, Computer
Science.\n\nAbstract\nEvery functor admitting an adjoint gives rise to can
onical factorization results. Classically\,\na functor with a left adjoint
factors through the category of Eilenberg–Moore algebras of\nthe induce
d monad\, while a functor with a right adjoint factors through the categor
y of\ncoalgebras of the induced comonad. Dually\, Kleisli and co-Kleisli c
onstructions provide\nfurther universal factorizations. \nEvery function
admits an image factorization. The lax analogue of this factorization is\n
the main subject of this talk. Working in a suitable 2-categorical setting
with opcomma\nobjects and pushouts\, every morphism admits a 2-dimensiona
l cokernel diagram which\, in\nthe presence of descent objects\, induces a
canonical descent factorization. This canonical\ndescent factorization ca
n\, and should\, be regarded as a lax version of the image factorization.
\nThis lax image factorization\, called lax semantic factorization\, sub
sumes the classical\nEilenberg–Moore and Kleisli factorizations. In part
icular\, it yields a novel result even in the\ncase of the 2-category Cat
of categories\, which is described below. \nEvery functor has a lax seman
tic factorization. When a functor has a left adjoint\, the\nlax semantic f
actorization (lax image factorization) coincides with the Eilenberg–Moor
e\nfactorization\; when it has a right adjoint\, it coincides with the coa
lgebraic factorization. \nThis work establishes another connection betwee
n monadicity and descent theory\, providing a formal counterpart to the cl
assical Bénabou–Roubaud theorem and leading to a\ngeneral monadicity th
eorem.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/67/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Giacomo Tendas (Manchester)
DTSTART:20260206T130000Z
DTEND:20260206T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/68
DESCRIPTION:Title: Logic internal to a monoidal closed category\nby Giacomo
Tendas (Manchester) as part of University of Birmingham theoretical comput
er science seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract
\nIn this talk I will explain how one can define notions of language and t
heory internal to a given (and sufficiently nice) category V endowed with
a tensor product. My motivation for this comes from enriched category t
heory\, where we use these theories on V to classify certain important cla
sses of categories enriched over V. For the purposes of this talk\, I will
focus on how the internal logic is defined (ignoring the enriched categor
ical aspects) and give several examples that hopefully will convince you o
f its usefulness. Important instances of V that I will discuss are the cat
egory of Posets\, that of Metric spaces\, and that of Small Categories.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/68/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Rice (University of Edinburgh)
DTSTART:20260213T130000Z
DTEND:20260213T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/69
DESCRIPTION:Title: A continuation monad for quantum effects in recursive program
s\nby Alex Rice (University of Edinburgh) as part of University of Bir
mingham theoretical computer science seminar\n\nLecture held in LG23\, Com
puter Science.\n\nAbstract\nThe semantics of pure quantum programs is well
understood\, and we have many tools for working with them. However\, many
modern quantum computing techniques\, such as variational algorithms\, qu
antum error correction\, and repeat-until-success circuits\, require hybri
d quantum-classical features\, where the semantics are not as clear.\n\n\n
In this talk\, I will represent these hybrid programs as classical program
s which can operate on quantum data by a computational effect. We show tha
t for non-recursive programs\, this effect can be described by so-called q
uantum instruments\, by showing that these devices can be given a monad st
ructure. The rest of the talk will then explore our path to generalising t
his monad to the category of complete partial orders\, which we desire for
describing the semantics of recursive hybrid programs. We note similariti
es to the probabilistic power-domain monad\, which has its multiplication
defined using an integral\, and I will explore our attempts to find a suit
able integral construction in our non-commutative setting. I will then pre
sent our solution based on continuations\, which effectively bypasses the
integral construction by instead axiomatising the properties we require fr
om it.\n\nI will assume no knowledge of quantum computing.\n\nJoint work w
ith Robert Booth\, Dominik Leichtle\, and Kim Worrall\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/69/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nihil Shah (University of Cambridge)
DTSTART:20260220T130000Z
DTEND:20260220T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/70
DESCRIPTION:Title: No-go theorems for distributive laws: directed containers vs.
uniform sampling\nby Nihil Shah (University of Cambridge) as part of
University of Birmingham theoretical computer science seminar\n\nLecture h
eld in LG23\, Computer Science.\n\nAbstract\nMonads model effectful comput
ation\, comonads model folding with a context. Given a comonad W and a mon
ad M\, when can two computations WA -> MB and WB -> MC be composed? Power
and Watanabe demonstrate that the existence of a mixed distributive law WM
-> MW gives a sufficient condition for obtaining a biKleisli category whe
re 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 no
t exist. I first show that\, on the category of sets\, there is no mixed d
istributive law of the non-empty list comonad over the powerset monad. We
then generalise the comonad demonstrating that a directed container W has
a distributive law over the powerset monad M if and only if W is a coreade
r comonad. Finally\, we generalise this no-go theorem to all monads over t
he category of sets which have a meaningful notion of "uniform sampling".
If I have time\, I will also go over transfer theorems which enable liftin
g these no-go theorems over Set to related (co)monads on a different categ
ory.\n\nThis talk is derived from my previous joint work with Amin Karamlo
u appearing in LICS 2024 (https://doi.org/10.1145/3661814.3662137).\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/70/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Elaine Pimentel (University College London)
DTSTART:20260227T130000Z
DTEND:20260227T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/71
DESCRIPTION:Title: Bilateralism with incompatible proofs and refutations\nby
Elaine Pimentel (University College London) as part of University of Birm
ingham theoretical computer science seminar\n\nLecture held in LG23\, Comp
uter Science.\n\nAbstract\nLogical bilateralism challenges traditional con
cepts of logic by treating assertion and denial as independent yet opposed
acts. While initially devised to justify classical logic\, its constructi
ve variants show that both acts admit intuitionistic interpretations. We w
ill present a bilateral system where a formula cannot be both provable and
refutable without contradiction\, offering a framework for modelling\nmat
hematical proofs and refutations that exclude inconsistency.\nWe formalise
the logic via a bilateral natural deduction system with the desirable pro
of-theoretic properties of normalisation\, subformula property and consist
ency\, together with a base-extension semantics grounded in explicit proof
s and refutations. Finally\, refutation is shown to coincide with Nelson's
constructive falsity\, extending intuitionistic logic for constructive ep
istemic reasoning.\n\nThis is a joint work with Victor Barroso-Nascimento
and Maria Osório\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/71/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Mrudula Balachander (University of Birmingham)
DTSTART:20260306T130000Z
DTEND:20260306T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/72
DESCRIPTION:Title: Towards practical synthesis based on automata learning and su
ccinct representations\nby Mrudula Balachander (University of Birmingh
am) as part of University of Birmingham theoretical computer science semin
ar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nReactive syste
ms continuously interact with their environment in real-time\, requiring h
igh standards of correctness\, reliability\, and efficiency. Designing suc
h systems is challenging due to their inherent complexity and the high ris
k of unexpected behavior or severe failures arising from unforeseen intera
ctions and\ntiming constraints. Therefore\, rigorous formal methods and ve
rification are needed to improve the reliability of reactive systems and e
nsure their correctness. The synthesis problem goes a step further and aim
s to automate the construction of reactive systems that are guaranteed to
meet a given specification\, typically expressed as logical formulas. This
dissertation advances the field of reactive system synthesis along two ma
in themes.\n\nFirst\, we address the limitations of automatic LTL synthesi
s by introducing “LTL synthesis with hints” — a novel variant of the
LTL synthesis problem that incorporates user guidance in the form of trac
es to steer synthesis algorithms toward more practical and efficient solut
ions. By generalizing the user-provided example traces\, our approach comb
ines passive learning techniques with existing LTL synthesis algorithms to
bridge the gap between abstract specifications and real-world implementat
ions\, as demonstrated through an implementation and a series of case stud
ies.\n\nSecond\, we investigate efficient and effective representations fo
r controllers. Traditional LTL synthesis algorithms output large finite-st
ate Mealy machines. To address the need for concise yet efficient represen
tation\, we explore the class of register automata\, which are finite stat
e machines equipped with registers\, recognising the class of regular lang
uages over infinite alphabets. Our work introduces a novel variant of dete
rministic register automata\, namely Register Automata with Permutations (
pDRA)\, which aims to strike a balance between succinctness and computatio
nal efficiency. Additionally\, we provide a Myhill–Nerode-like character
isation that enables the construction of canonical minimal representations
. Furthermore\, we present a polynomial-time passive learning algorithm fo
r a subclass of these automata\, demonstrating the efficient identificatio
n of this class in the limit [63].\n\nTogether\, these contributions enhan
ce the practicality and scalability of synthesising reactive systems throu
gh LTL specifications\, paving the way for more robust and manageable impl
ementations in real-world applications.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/72/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Pedro Azevedo De Amorim (University of Bath)
DTSTART:20260313T130000Z
DTEND:20260313T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/73
DESCRIPTION:Title: A 2-categorical theory of logical relations\nby Pedro Aze
vedo De Amorim (University of Bath) as part of University of Birmingham th
eoretical computer science seminar\n\nLecture held in LG23\, Computer Scie
nce.\n\nAbstract\nLogical relations are a key tool in the semanticist's to
olkit. They play a central role in proofs of adequacy\, in characterizing
definability\, and in comparing different interpretations of the same comp
utational effect. From a denotational perspective\, logical relations are
elegantly captured by "fibrations for logical relations". These are Grothe
ndieck fibrations which strictly preserve the interpretation of types. Thi
s theory is well-developed for models of the simply-typed lambda calculus
and monadic-style CBV languages with effects\, but it is not obvious how t
o extend it to other kinds of modal calculi.\n\nIn this talk I will outlin
e the existing theory\, then show how taking a 2-categorical perspective l
eads naturally to a mathematically-justified definition of fibration---and
hence logical relations---for a wide variety of modal languages\, includi
ng Levy's call-by-push-value.\n\nNo prior knowledge of 2-category theory o
r fibrations will be assumed.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/73/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Silvia Butti (King's College London)
DTSTART:20260320T130000Z
DTEND:20260320T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/74
DESCRIPTION:Title: The Weisfeiler–Leman Dimension of Relational Database Queri
es\nby Silvia Butti (King's College London) as part of University of B
irmingham theoretical computer science seminar\n\nLecture held in LG23\, C
omputer Science.\n\nAbstract\nIn this work we investigate the expressive p
ower of the k-variable counting logic C^k on relational structures without
arity constraints and its implications for database query languages. \n\n
Existing results are limited to graphs or to C^2. In our setting\, we cons
ider the operation of a relational version of the Weisfeiler-Leman (WL) al
gorithm on structures of arbitrary rank. The (k-1)-dimensional WL algorith
m is known to have the same expressive power as C^k\, and\, through this l
ink\, the WL dimension is an established measure in descriptive complexity
theory. Specifically\, the WL dimension of a query \\varphi denotes the m
inimum dimension of the WL algorithm that distinguishes relational structu
res with different numbers of answers to \\varphi. \n\nOur central technic
al contribution is the introduction and analysis of a novel Cai-Fürer-Imm
erman type of construction for general relational structures. Building on
this\, our results are threefold.\nFirst\, we determine the WL dimension o
f full conjunctive queries over arbitrary signatures\, and we provide boun
ds on it for general conjunctive queries. Second\, we show that the number
of answers to a conjunctive query of WL dimension k in a relational datab
ase D can 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
expressivity of Datalog queries.\n\nJoint work with A. Göbel\, L. A. Gol
dberg\, S. Kiefer\, M. Lanzinger\, and M. Roth\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/74/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nicholas Pischke (University of Bath)
DTSTART:20260327T130000Z
DTEND:20260327T140000Z
DTSTAMP:20260404T131157Z
UID:TheoryCSBham/75
DESCRIPTION:Title: An overview of proof mining and probability theory\nby Ni
cholas Pischke (University of Bath) as part of University of Birmingham th
eoretical computer science seminar\n\nLecture held in LG23\, Computer Scie
nce.\n\nAbstract\nOn the surface\, the theory of probability measures requ
ires the use of proof-theoretically strong principles to already develop s
ome of the most basic notions. Contrary to these apparent limitations\, an
approach for extending the program of proof mining to this area has recen
tly been proposed. This approach\, which is fundamentally based on the use
of probability contents (i.e.\, finitely additive [0\, 1]-valued function
s defined on algebras of sets)\, has proven to be widely effective based o
n a range 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 e
ndeavour\, as well as recent applications to stochastic analysis and optim
ization which rely on these methods. The talk is based on various (joint)
works\, in collaboration with Morenikeji Neri\, Paulo Oliva and Thomas Pow
ell.\n
LOCATION:https://stable.researchseminars.org/talk/TheoryCSBham/75/
END:VEVENT
END:VCALENDAR