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:20240224T073058Z
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:20240224T073058Z
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:20240224T073058Z
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:20240224T073058Z
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:20240224T073058Z
UID:TheoryCSBham/5
DESCRIPTION:by Nesta Van Der Schaaf (University of Edinburgh) as part of U
niversity of Birmingham theoretical computer science seminar\n\nInteractiv
e livestream: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0R
LL2RlTzFBam1IUT09\nLecture held in LG23\, Computer Science.\nAbstract: TBA
\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/5/
URL:https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBa
m1IUT09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Charles Grellois (University of Sheffield)
DTSTART;VALUE=DATE-TIME:20240308T110000Z
DTEND;VALUE=DATE-TIME:20240308T120000Z
DTSTAMP;VALUE=DATE-TIME:20240224T073058Z
UID:TheoryCSBham/6
DESCRIPTION:by Charles Grellois (University of Sheffield) as part of Unive
rsity of Birmingham theoretical computer science seminar\n\nInteractive li
vestream: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2R
lTzFBam1IUT09\nLecture held in LG23\, Computer Science.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/6/
URL:https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBa
m1IUT09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leo Lobski (University College London)
DTSTART;VALUE=DATE-TIME:20240315T110000Z
DTEND;VALUE=DATE-TIME:20240315T120000Z
DTSTAMP;VALUE=DATE-TIME:20240224T073058Z
UID:TheoryCSBham/7
DESCRIPTION:by Leo Lobski (University College London) as part of Universit
y of Birmingham theoretical computer science seminar\n\nInteractive livest
ream: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzF
Bam1IUT09\nLecture held in LG23\, Computer Science.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/7/
URL:https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBa
m1IUT09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Luca Reggio (University College London)
DTSTART;VALUE=DATE-TIME:20240322T110000Z
DTEND;VALUE=DATE-TIME:20240322T120000Z
DTSTAMP;VALUE=DATE-TIME:20240224T073058Z
UID:TheoryCSBham/8
DESCRIPTION:by Luca Reggio (University College London) as part of Universi
ty of Birmingham theoretical computer science seminar\n\nInteractive lives
tream: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTz
FBam1IUT09\nLecture held in LG23\, Computer Science.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/8/
URL:https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBa
m1IUT09
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bartek Klin (University of Oxford)
DTSTART;VALUE=DATE-TIME:20240426T100000Z
DTEND;VALUE=DATE-TIME:20240426T110000Z
DTSTAMP;VALUE=DATE-TIME:20240224T073058Z
UID:TheoryCSBham/9
DESCRIPTION:by Bartek Klin (University of Oxford) as part of University of
Birmingham theoretical computer science seminar\n\nInteractive livestream
: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1
IUT09\nLecture held in LG23\, Computer Science.\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/TheoryCSBham/9/
URL:https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBa
m1IUT09
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:20240224T073058Z
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
END:VCALENDAR