BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Jeremy Gibbons (University of Oxford)
DTSTART;VALUE=DATE-TIME:20240126T110000Z
DTEND;VALUE=DATE-TIME:20240126T120000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/1
DESCRIPTION:Title: Turner\, Bird\, Eratosthenes: An Eternal Burning Thread\nby Jerem
y Gibbons (University of Oxford) as part of University of Birmingham theor
etical computer science seminar\n\nLecture held in LG23\, Computer Science
.\n\nAbstract\nThe late David Turner had great taste in language design an
d programming\; the design decisions he made in his languages SASL \, KRC\
, and Miranda over the last 50 years are still influential now. One exampl
e program that he introduced to illustrate lazy evaluation and list compre
hensions in SASL is a one-line recursive “sieve” to generate the infin
ite list of prime numbers.\n\nTurner called this algorithm The Sieve of Er
atosthenes. However\, in a lovely paper “The Genuine Sieve of Eratosthen
es” (JFP\, 2009)\, Melissa O’Neill argued that Turner’s algorithm is
not faithful to Eratosthenes\, and gave a detailed presentation using pri
ority queues of the real thing. She included a variation by Richard Bird\,
that uses only lists but makes clever use of circular programming. Bird d
escribes his circular program again in his textbook “Thinking Functional
ly with Haskell”\, and sets its proof of correctness as an exercise. Unf
ortunately\, his hint for a solution is incorrect. So what should a proof
look like?\n\nOne of the last projects Turner worked on was the notion of
“Total Functional Programming” (eg J.UCS\, 2004)\, “designed to excl
ude the possibility of non-termination”. He observed that most programs
are already structurally recursive or corecursive\, therefore guaranteed t
erminating or productive respectively\, and conjectured that “with more
practice we will find this is always true”. Much as I find this idea app
ealing\, I think we are still some way off\, even after 20 years of “mor
e practice”. I will discuss Bird’s circular Sieve of Eratosthenes as a
challenge problem for Turner’s Total FP.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tomáš Jakl (Czech Academy of Sciences / Czech Technical Universi
ty)
DTSTART;VALUE=DATE-TIME:20240202T110000Z
DTEND;VALUE=DATE-TIME:20240202T120000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/2
DESCRIPTION:Title: Feferman–Vaught–Mostowski theorems and game comonads\nby Tom
áš Jakl (Czech Academy of Sciences / Czech Technical University) as part
of University of Birmingham theoretical computer science seminar\n\nLectu
re held in LG23\, Computer Science.\n\nAbstract\nIn recent years we have s
een a growing number of examples of model\ncomparison games (such as pebbl
e games or Ehrenfreucht-Fraisse games)\nbeing encoded semantically\, as co
monads on the class of graphs or\nrelational structures. Apart from the co
nnections with logic (via the\nmodel comparison games)\, game comonads can
also express a range of\nimportant parameters in finite model theory and
combinatorics\, such as\ntree-width and tree-depth.\n\nAfter a brief overv
iew of the emerging theory of game comonads\, I\nwill present my joint wor
k with Dan Marsden and Nihil Shah. Our main\nfocus are the so-called Fefer
man–Vaught-Mostowski-type theorems\, which\nexpress when an operation on
models preserves equivalence in a given logic.\n\nProving these theorems
in the comonadic setting amounts to defining\na Kleisli law and checking c
ertain smoothness conditions. Surprisingly\,\nthe main ingredient of our a
pproach is a generalisation of how monoidal\nmonads lift the monoidal stru
cture to the category of algebras.\nFurthermore\, we also show the role of
bilinear maps in this setting and\nhow Johnstone's adjoint lifting theore
m is a special case of all this.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dylan Braithwaite (University of Strathclyde)
DTSTART;VALUE=DATE-TIME:20240216T110000Z
DTEND;VALUE=DATE-TIME:20240216T120000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/3
DESCRIPTION:Title: Probabilistic Programming with Session Types\nby Dylan Braithwait
e (University of Strathclyde) as part of University of Birmingham theoreti
cal computer science seminar\n\nLecture held in LG23\, Computer Science.\n
\nAbstract\nStatistical inference algorithms often involve an interactive
flow of information. The fundamental principle behind Bayesian statistics
can be seen as an interactive process where a model consists of a likeliho
od function\, which makes a prediction based on some prior knowledge\, and
later receives observations or updates\, as proposed improvements to its
predictions. Similarly\, the idea of interventions in causal inference has
been explained (see Jacobs\, Kissinger and Zanasi) as a kind of factorisa
tion of a Markov kernel into a kernel with additional input and outputs\,
with certain causal relationship encoding the ideal that the inputs occur
after certain outputs.\n\nInteractive protocols of this sort\, with interl
eaved inputs and outputs\, have been modelled in programming languages wit
h session types: type systems for a process calculus which encode encode s
equences of sets annotated with input/output information. Typically semant
ic models of session types make use of an encoding into linear logic\, all
owing process specifications to be interpreted in *-autonomous categories.
Unfortunately\, categories of probabilistic spaces do not usually have su
ch structure\, and so are not suitable for as a full model of linear logic
\, but this structure is far from necessary for modelling simple I/O seque
nces. Recently categorical notions of "combs" have been proposed by severa
l authors as a model for such interactive processes: they provide a genera
l compositional model for processes with sequenced I/O which can be constr
ucted over any monoidal category.\n\nIn this talk I will explain how typic
al operations used in statistical inference algorithms can be succinctly r
epresented as operations on combs\, and outline a description of a simple
language with session types to be interpreted in a (multi)category of comb
s\, and explore how this can be used as a novel form of probabilistic prog
ramming language.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/3/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Kavvos (University of Bristol)
DTSTART;VALUE=DATE-TIME:20240223T110000Z
DTEND;VALUE=DATE-TIME:20240223T120000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/4
DESCRIPTION:Title: Two-dimensional Kripke Semantics\nby Alex Kavvos (University of B
ristol) as part of University of Birmingham theoretical computer science s
eminar\n\nLecture held in G33\, Aston Webb.\n\nAbstract\nThe study of moda
l logic has witnessed tremendous development following the introduction of
Kripke semantics. However\, recent developments in programming languages
and type theory have led to a second way of studying modalities\, namely t
hrough their categorical semantics. We show how the two correspond.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nesta van der Schaaf (University of Edinburgh)
DTSTART;VALUE=DATE-TIME:20240301T110000Z
DTEND;VALUE=DATE-TIME:20240301T120000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/5
DESCRIPTION:Title: Ordered Locales\nby Nesta van der Schaaf (University of Edinburgh
) as part of University of Birmingham theoretical computer science seminar
\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nOrder and topolo
gy both abound in mathematics\, often even together. Combined\, they form
the notion of an ordered topological space. How can this notion be suitabl
y generalised to the theory of point-free topology? In this talk we will d
iscuss one possibility\, based on the so-called Egli-Milner relation. To k
eep the talk accessible\, we start with an introduction to the definition
of locales and describe their adjunction with topological spaces. After th
at\, we show how this adjunction can be extended to certain categories of
ordered spaces and the newly introduced ordered locales. To finish the tal
k we highlight some ongoing work. First\, we describe how we are using the
se techniques to study aspects of relativity theory. In particular\, we de
scribe ingredients for a "causal boundary" construction\, and show how "do
mains of dependence" can be recovered as a natural Grothendieck topology o
n ordered locales. Lastly\, time permitting\, we discuss an "internal" gen
eralisation of ordered locales. (Based on joint work with Chris Heunen and
Prakash Panangaden.)\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Charles Grellois (University of Sheffield)
DTSTART;VALUE=DATE-TIME:20240308T110000Z
DTEND;VALUE=DATE-TIME:20240308T120000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/6
DESCRIPTION:Title: Semantic approaches to verification of functional programs\nby Ch
arles Grellois (University of Sheffield) as part of University of Birmingh
am theoretical computer science seminar\n\nLecture held in LG23\, Computer
Science.\n\nAbstract\nWhat can the semantics of a program bring when it c
omes to verification? Almost a decade ago\, during my PhD under the superv
ision of Paul-André Melliès\, we showed that the main problem considered
in higher-order model-checking could be actually reduced to computing the
semantics of the program in some models of linear logic\, enriched with a
modality and a tricky inductive-coinductive fixpoint operator. Decidabili
ty would follow from the existence of finitary models in which this "seman
tic verification procedure" is possible.\n\nAn interesting point in this a
pproach is that this "practical" problem from verification leads us to act
ually consider new and very relevant extensions of the semantics of linear
logic\, notably since the higher-order model-checking problem requires mi
xing inductive and coinductive reasoning\; but the interplay of programs a
nd alternating tree automata is also surprisingly natural at the light of
linear logic.\n\nThe "original" higher-order model-checking problem was pr
oved decidable by Ong in 2006\; it led to many alternative proofs\, explor
ing a vast area of theoretical computer science. I believe that this explo
ration is far from over\, and will discuss new potential directions involv
ing cyclic proofs\, infinitary reasoning\, extensional collapses...\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leo Lobski (University College London)
DTSTART;VALUE=DATE-TIME:20240315T110000Z
DTEND;VALUE=DATE-TIME:20240315T120000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/7
DESCRIPTION:Title: Towards functorial chemistry: completeness and universality for react
ion representation\nby Leo Lobski (University College London) as part
of University of Birmingham theoretical computer science seminar\n\nLectur
e held in LG23\, Computer Science.\n\nAbstract\nOrganic molecules can be r
epresented mathematically using labelled graphs [1]. Recently\, the graph
approach to chemistry has been extended to reactions using the techniques
of graph rewriting [2\,3]. While representing reactions lies at the heart
of mathematical chemistry\, the focus to date has been on the "forward" di
rection of reaction prediction and composition. The "reverse" direction of
discovering reaction pathways to new compounds is\, however\, one of the
main aims of modern chemical engineering. The methodology of this field\,
known as retrosynthetic analysis\, is well-established and widely practise
d [4\,5\,6\,7]\, but has received significantly less mathematical attentio
n.\n\nIn this talk\, I will suggest taking the basic units of retrosynthet
ic analysis - disconnection rules - as first-class citizens of reaction re
presentation. The mathematical and conceptual justification for doing so l
ies in the fact that both disconnection rules and formalised reactions can
be arranged into monoidal categories [8]\, such that there is a monoidal
functor taking each (composable) sequence of disconnection rules to a reac
tion. Our main result shows that\, under a certain axiomatisation of the d
isconnection rules\, the functor is faithful and an opfibration. This impl
ies that every reaction can be decomposed into a sequence of disconnection
rules (universality) in an essentially unique way (completeness).\n\n[1]
D. Bonchev and D.H. Rouvray (eds). Chemical Graph Theory: Introduction and
Fundamentals. Abacus Press / Gordon & Breach Science Publishers. 1991.\n\
n[2] J.L. Andersen\, C. Flamm\, D. Merkle\, and P.F. Stadler. Inferring ch
emical reaction patterns using rule composition in graph grammars. J. Syst
. Chem. 2013.\n\n[3] J.L. Andersen\, C. Flamm\, D. Merkle\, and P.F. Stadl
er. An intermediate level of abstraction for computational systems chemist
ry. Philos. Trans. R. Soc. 2017.\n\n[4] E.J. Corey and X. Cheng. The logic
of chemical synthesis. John Wiley. 1989.\n\n[5] S. Warren and P. Wyatt. O
rganic synthesis: the disconnection approach. Wiley. 2008.\n\n[6] J. Clayd
en\, N. Greeves\, and S. Warren. Organic chemistry. OUP. 2012.\n\n[7] Y. S
un and N.V. Sahinidis. Computer-aided retrosynthetic design: fundamentals\
, tools\, and outlook. Curr. Opin. Chem. Eng. 2022.\n\n[8] E. Gale\, L. Lo
bski\, and F. Zanasi. A Categorical Approach to Synthetic Chemistry. Theor
etical Aspects of Computing - ICTAC. 2023.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Cristina Matache (University of Edinburgh)
DTSTART;VALUE=DATE-TIME:20240322T110000Z
DTEND;VALUE=DATE-TIME:20240322T120000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/8
DESCRIPTION:Title: Parameterized algebraic theories and applications\nby Cristina Ma
tache (University of Edinburgh) as part of University of Birmingham theore
tical computer science seminar\n\nLecture held in LG23\, Computer Science.
\n\nAbstract\nThe framework of algebraic theories has proved useful for re
asoning equationally about impure computation\, such as state\, nondetermi
nism\, probabilistic choice. In this talk\, I will review parameterized al
gebraic theories\, an extension of algebraic theories that allows for bind
ing. I will show how parameterized theories can be used to give an equatio
nal account of scoped effects\, a class of effects that does not fit into
the plain algebraic framework. Finally\, I will sketch work in progress ab
out axiomatizing dynamic creation of threads using parameterized theories.
\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/8/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Pablo Donato (École Polytechnique)
DTSTART;VALUE=DATE-TIME:20240419T100000Z
DTEND;VALUE=DATE-TIME:20240419T110000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/9
DESCRIPTION:Title: Deep Inference for Graphical Theorem Proving\nby Pablo Donato (É
cole Polytechnique) as part of University of Birmingham theoretical comput
er science seminar\n\nLecture held in TBA.\n\nAbstract\nIn this talk\, I w
ill summarize my four-year thesis journey focused on designing graphical u
ser interfaces (GUIs) for interactive proof construction. Deep inference p
roof theory guided my approach\, inspiring innovative representations and
interactions with logical entities.\n\nThe first part of the talk will int
roduce the Proof-by-Action paradigm\, enabling users to construct proofs t
hrough direct manipulation of the proof state. Actema\, a GUI prototype fo
r intuitionistic first-order logic\, demonstrates this approach with its d
rag-and-drop proof tactic grounded in "subformula linking"\, a recent tech
nique based on the calculus of structures.\n\nIn the subsequent discussion
\, I will present an open-ended line of research where I aim to get rid of
traditional symbolic formulas\, in favor of more structured and iconic re
presentations of the proof state. This includes the development of so-call
ed "bubble calculi"\, a family of systems that reframe and extend the theo
ry of nested sequents as local rewriting systems. Bubble calculi enjoy a g
raphical and topological interpretation\, enable efficient sharing of cont
exts among subgoals\, and capture both intuitionistic\, dual-intuitionisti
c\, bi-intuitionistic and classical logic in a unified way.\n\nFinally\, I
will introduce the flower calculus\, an intuitionistic refinement of C.S.
Peirce's theory of existential graphs\, understood as a system for intera
ctive proof building. It provides more iconic and economical means of reas
oning than bubble calculi\, by exposing a small number of expressive rules
that apply to the goals themselves\, removing completely the need for log
ical connectives. I will conclude with a demonstration of the Flower Prove
r\, another prototype of GUI in the Proof-by-Action paradigm\, whose actio
ns map directly to the rules of the flower calculus.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Satoshi Kura (National Institute of Informatics / University of Ox
ford)
DTSTART;VALUE=DATE-TIME:20240209T110000Z
DTEND;VALUE=DATE-TIME:20240209T120000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/10
DESCRIPTION:Title: Higher-Order Weakest Precondition Transformers via a CPS Transformat
ion\nby Satoshi Kura (National Institute of Informatics / University o
f Oxford) as part of University of Birmingham theoretical computer science
seminar\n\nLecture held in LG23\, Computer Science.\n\nAbstract\nWeakest
preconditions are essential notions for program verification. There are ma
ny variations of weakest preconditions\, and their uniform treatment has b
een studied using category-theoretic notions like monads. In this talk\, w
e consider weakest preconditions for a higher-order functional language wi
th computational effects and recursion and show that we can syntactically
compute them via a CPS transformation. We prove our main theorem in a gene
ral setting\, which enables us to instantiate our result to several proble
ms of program verification. Our result generalises two existing works on p
rogram verification: (1) trace properties and may-/must-reachability studi
ed by Kobayashi et al. and (2) expected cost analyses studied by Avanzini
et al. We also obtain a new instance of cost moment analyses using our mai
n theorem.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Igor Carboni Oliveira (University of Warwick)
DTSTART;VALUE=DATE-TIME:20240318T130000Z
DTEND;VALUE=DATE-TIME:20240318T140000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/11
DESCRIPTION:Title: Polynomial-Time Pseudodeterministic Construction of Primes\nby I
gor Carboni Oliveira (University of Warwick) as part of University of Birm
ingham theoretical computer science seminar\n\nLecture held in LG23\, Comp
uter Science.\n\nAbstract\nA randomized algorithm for a search problem is
pseudodeterministic if it produces a fixed canonical solution to the searc
h problem with high probability. In their seminal work on the topic\, Gat
and Goldwasser posed as their main open problem whether prime numbers can
be pseudodeterministically constructed in polynomial time.\n\nWe provide a
positive solution to this question in the infinitely-often regime. In mor
e detail\, we give an unconditional polynomial-time randomized algorithm $
B$ such that\, for infinitely many values of $n$\, $B(1^n)$ outputs a cano
nical $n$-bit prime $p_n$ with high probability. More generally\, we prove
that for every dense property $Q$ of strings that can be decided in polyn
omial time\, there is an infinitely-often pseudodeterministic polynomial-t
ime construction of strings satisfying $Q$. This improves upon a subexpone
ntial-time construction of Oliveira and Santhanam.\n\nOur construction use
s several new ideas\, including a novel bootstrapping technique for pseudo
deterministic constructions\, and a quantitative optimization of the unifo
rm hardness-randomness framework of Chen and\nTell\, using a variant of th
e Shaltiel-Umans generator.\n\nReference: https://eccc.weizmann.ac.il/repo
rt/2023/076/\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hugo Ferée (IRIF)
DTSTART;VALUE=DATE-TIME:20240418T100000Z
DTEND;VALUE=DATE-TIME:20240418T110000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/12
DESCRIPTION:Title: Mechanised uniform interpolation for modal logics K\, GL and iSL
\nby Hugo Ferée (IRIF) as part of University of Birmingham theoretical co
mputer science seminar\n\nLecture held in Old Gym LG06.\n\nAbstract\nThe u
niform interpolation property in a given logic can be understood as the de
finability of propositional quantifiers. We will describe here proof-theor
etic proof of this property for three modal logics: iSL (for which this is
a new result)\, K and GL (for which we fixed an issue in the existing pro
of). All three proofs are implemented in the Coq proof assistant\, making
the computation of the interpolants effective.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Andrew Sogokon (Lancaster University)
DTSTART;VALUE=DATE-TIME:20240510T100000Z
DTEND;VALUE=DATE-TIME:20240510T110000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/14
DESCRIPTION:Title: Inductive Invariants in Continuous Systems\nby Andrew Sogokon (L
ancaster University) as part of University of Birmingham theoretical compu
ter science seminar\n\nLecture held in Aston Webb\, WG12.\n\nAbstract\nThe
problem of checking whether a set is an inductive invariant is of fundame
ntal importance to formal safety verification. While the tools required fo
r this problem in the typical discrete setting are rather straightforward
and quite standard in computer science\, the situation is markedly differe
nt in continuous systems (i.e. systems where time does not advance in disc
rete time steps\, but instead passes continuously\, e.g. as in systems def
ined by ordinary differential equations). This problem was considered by m
athematicians since the 1940s\, who developed several characterizations wh
ich\, unfortunately\, do not provide an effective way of checking whether
a given set is an inductive invariant for a given continuous system. In th
e past decade great progress has been made by computer scientists in devel
oping the tools for reasoning about continuous systems and powerful result
s have been reported which essentially solve the problem of inductive inva
riant checking algorithmically under some reasonable restrictions on the n
ature of the set and the kind of continuous system. In this talk\, I will
present an overview of some of the progress that has been made and will ou
tline some fundamental practical limitations inherent in current approache
s.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Calum Hughes (University of Manchester)
DTSTART;VALUE=DATE-TIME:20240517T100000Z
DTEND;VALUE=DATE-TIME:20240517T110000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/15
DESCRIPTION:Title: Models of Martin-Löf Type Theory and Algebraic Model Structures
\nby Calum Hughes (University of Manchester) as part of University of Birm
ingham theoretical computer science seminar\n\nLecture held in Aston Webb\
, WG12.\n\nAbstract\nKnown models of Martin-Löf Type Theory (MLTT) includ
e isofibrations in the category of groupoids and Kan fibrations in the cat
egory of simplicial sets. It is an open problem to prove constructively th
at Kan fibrations model Homotopy Type Theory. One suggested way to approac
h this problem is with an algebraic perspective\; the idea being that by k
eeping track of the algebraic data throughout calculations\, proofs become
more constructive. Classically\, normal isofibrations are the algebras fo
r the right class of a type theoretic algebraic weak factorisation system
which form part of an algebraic model structure. Constructively\, however\
, this link breaks down as this algebraic model structure fails to exist.\
n\nIn this talk\, I will show how we can re-establish this connection by p
roving constructively that cloven isofibrations are the algebras for the r
ight class of a type theoretic algebraic weak factorisation system which f
orm part of an algebraic model structure. I will also briefly discuss how
this result holds more generally\, providing an internal-groupoidal model
of MLTT with links to an algebraic model structure.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sam van Gool (IRIF\, Paris)
DTSTART;VALUE=DATE-TIME:20240524T100000Z
DTEND;VALUE=DATE-TIME:20240524T110000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/16
DESCRIPTION:Title: Deciding unifiability by folding coalgebras\nby Sam van Gool (IR
IF\, Paris) as part of University of Birmingham theoretical computer scien
ce seminar\n\nLecture held in Aston Webb\, WG12.\n\nAbstract\nThe unifiabi
lity problem for a logic L asks to decide whether or not\nthere exists a s
yntactic substitution that renders two given formulas\nequivalent in L.\n\
nThe first objective of this talk is to show how the unifiability problem\
nfor a logic can often be usefully reformulated as a problem about\nhomomo
rphisms between coalgebras.\n\nThe second objective is to showcase this me
thod in the context of the\ntemporal logic of next\, that is\, classical p
ropositional logic with a\ndeterministic unary modality. In this specific
case\, we show that the\nunifiability problem is equivalent to a homomorph
ism mapping problem for\na sequence of graphs known in the literature as D
e Bruijn graphs. We\nsolve the homomorphism mapping problem\, employing me
thods rooted in\nstring compression\, and thus establishing decidability o
f unifiability\nfor the temporal logic of next.\n\nThis work is part of an
ongoing collaboration with Johannes Marti and\nMichelle Sweering.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/16/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ambroise Lafont (École Polytechnique)
DTSTART;VALUE=DATE-TIME:20240531T100000Z
DTEND;VALUE=DATE-TIME:20240531T110000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/17
DESCRIPTION:Title: A diagram editor to mechanise categorical proofs\nby Ambroise La
font (École Polytechnique) as part of University of Birmingham theoretica
l computer science seminar\n\nLecture held in LG23\, Computer Science.\n\n
Abstract\nDiagrammatic proofs are ubiquitous in certain areas of mathemati
cs\, especially in category theory. Mechanising such proofs is a tedious t
ask because proof assistants (such as Coq) are text based. We present a pr
ototypical diagram editor to make this process easier\, building upon the
vscode extension coq-lsp for the Coq proof assistant and a web application
(https://amblafont.github.io/graph-editor/index.html).\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Paul Taylor (University of Birmingham)
DTSTART;VALUE=DATE-TIME:20240426T100000Z
DTEND;VALUE=DATE-TIME:20240426T110000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/18
DESCRIPTION:Title: Free algebras for functors\, with not an ordinal in sight\nby Pa
ul Taylor (University of Birmingham) as part of University of Birmingham t
heoretical computer science seminar\n\nLecture held in Old Gym\, LG10.\n\n
Abstract\nMartin Escardo challenged me to make Pataraia's fixed point\nthe
orem "predicative". Whilst I have never understood the\nmotivation for th
at notion\, I have eliminated one instance\nof impredicativity and isolate
d the infinitary aspects to\na single specific directed join.\n\nSo then I
looked for the categorical version. Pataraia's\nidea plays a quite small
part: the construction uses ideas\nfrom categorical algebra since its orig
ins\, and if I were\nto credit one person it would be Joachim Lambek.\n\nT
he problem breaks into two parts\, one finitary and the\nother infinitary.
The infinitary part says that the\ncategory of pointed endofunctors of a
small category\nwith coequalisers is filtered\, so has a terminal object\
nif the given category has the required filtered colimit.\nThis is probabl
y widely applicable as an alternative to\ntransfinite methods.\n\nThe fini
tary construction is that of fragments of the\ninitial algebra. It may be
done in several ways\, but\none is to consider coalgebras for the given f
unctor\nthat are have a cone over all algebras for it. We\nidentify a "sp
ecial condition" that this construction\nsatisfies and that ensures that t
he terminal endofunctor\n(applied to any object) yields the terminal objec
t of\nthe finitary category\, which is the required initial\nalgebra of th
e functor.\n\nThe hope is that a similar finitary category of\npartial mod
els could be found for more complex\nsystems of algebra and logic and that
these would\ncorrespond to the intermediate stages in proof\ntheoretic ar
guments for normalisation\, cut\nelimination etc.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Wilmer Ricciotti (University of Edinburgh)
DTSTART;VALUE=DATE-TIME:20240607T100000Z
DTEND;VALUE=DATE-TIME:20240607T110000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/19
DESCRIPTION:Title: Syntactic representation of program execution history\nby Wilmer
Ricciotti (University of Edinburgh) as part of University of Birmingham t
heoretical computer science seminar\n\nLecture held in LG23\, Computer Sci
ence.\n\nAbstract\nAuditing is an increasingly important operation for com
puter programming\, for example in security (e.g. to enable history-based
access control) and to enable reproducibility and accountability (e.g. pro
venance in scientific programming). Engineering a software system to allow
history-based auditing by means of ad-hoc instrumentation requires a subs
tantial effort: the development of general-purpose infrastructure is thus
very important to achieve the goal of making such techniques widely availa
ble.\n\nInspired by work on Justification Logic\, we study the syntactic r
epresentation of program execution history in the setting of the Calculus
of Audited Units\, a core functional language providing auditing as a firs
t-class operation. CAU automatically materializes execution history as a d
ata structure and can be implemented by a call-by-value abstract machine i
n a relatively efficient way. To prove the correctness of our machine\, we
extend the language with explicit substitutions and explicit auditing ope
rations.\n\nWe discuss applications of auditing by showing how to use it t
o derive various provenance views relating program output to its input. Fi
nally\, we present some current work showing a connection between the synt
actic representation of execution history and the standardisation theorem
for the lambda calculus.\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Georg Struth (University of Sheffield)
DTSTART;VALUE=DATE-TIME:20240621T100000Z
DTEND;VALUE=DATE-TIME:20240621T110000Z
DTSTAMP;VALUE=DATE-TIME:20240715T184638Z
UID:TheoryCSBham/20
DESCRIPTION:Title: Formalising globular and cubical categories with a proof assistant\nby Georg Struth (University of Sheffield) as part of University of Bir
mingham theoretical computer science seminar\n\nLecture held in LG23\, Com
puter Science.\n\nAbstract\nFor applications in higher-dimensional rewriti
ng\, we have\nrecently formalised globular and cubical categories with the
\nIsabelle/HOL proof assistant. In the literature\, globular categories\,\
n(aka strict n- or omega-categories) are often defined in single-set\nstyl
e\, where only a set of arrows is given\, and objects arise\nindirectly as
fixpoints of source and target maps. In this talk I will\nfirst explain w
hy and how we have formalised this approach with\nIsabelle. In the cubical
case\, a single-set axiomatisation has so far\nbeen missing. Here I show
how Isabelle/HOL has been instrumental in\nfinding one\, allowing us to ta
me a large number of initial candiate\naxioms. I will also discuss the cat
egorical equivalence proofs\n(outside of Isabelle) that justify the correc
tness of our axioms\nrelative to the standard ones by Al Agl\, Brown and S
teiner.\n\nIn combination\, these examples present a case study in experim
ental\nmathematics with a proof assistant. In my talk I will focus on the\
nformalisation experience -- lights and shadows -- and conclude with\nsome
general remarks about formalised mathematics.\n\nThis is joint work with
Cameron Calk (Aix-Marseille Université)\, \nDamien Pous (ENS Lyon) Philip
pe Malbos and Tanguy Massacrier \n(Université Claude Bernard Lyon 1). It
is based on the articles\n\nhttps://arxiv.org/pdf/2307.09253\n\nhttps://ar
xiv.org/pdf/2401.10553\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/20/
END:VEVENT
END:VCALENDAR