Indeed\nntly Shulman has proposed a nearly identical structure under the name ‘LNL-polycategories’. Shulman shows that by asking that different collections of universal properties be present\, LNL-polycategories may be used as a model for the LNL calculus\, CBPV\, and other models of effectful calculi. Inspired by this I will survey the universal properties required for implementing the basic communication primitives in a process calculus. With this framework\, we can compare process models with the structures present in linear logic models\, or effectful models\, offering an additional perspective into the existing connections between the pi-calculus and linear logic or algebraic effects.\n\n UID:398 END:VEVENT BEGIN:VEVENT DTSTAMP;TZID=Europe/London:20241110T132647 DTSTART;TZID=Europe/London:20240405T150000 DTEND;TZID=Europe/London:20240405T160000 LOCATION:LT209 and Online SUMMARY:I Think Indexed Enriched Categories are Nice. DESCRIPTION:Speaker: Jade Master (MSP)\nTitle: I Think Indexed Enriched Categories are Nice.\n\nFirst proposed by Lawvere in 1973\, indexed enriched categories are a very complicated mathematical structure studied in only the most privileged ivory towers. In this talk I intend to bring them down to earth by exploring their viability as a data structure. I will cheat by only considering enrichments where the axioms are satisfied trivially. I will explain how these 'trivial' enriched categories are nice data structures for holding solutions to algebraic path problems. Then I will explain how making them indexed allows us to work with distributed\, concurrent\, and compositional algebraic path problems. This talk will be in line with the research programme I started to develop before I quit and left for industry. Namely\, that indexed categories and Grothendieck constructions may be used to develop a general theory of compositional computation. This talk will feature Idris2 code and categorical terminology side-by-side so that those familiar with either language will be able to follow along.\n UID:397 END:VEVENT BEGIN:VEVENT DTSTAMP;TZID=Europe/London:20241110T132647 DTSTART;TZID=Europe/London:20240322T150000 DTEND;TZID=Europe/London:20240322T160000 LOCATION:LT209 and Online SUMMARY:Softmax is Argmax\, and the Logic of the Reals DESCRIPTION:Speaker: Matteo Capucci (MSP)\nTitle: Softmax is Argmax\, and the Logic of the Reals\n\nI will report some work in progress on the semiotics of softmax. This is an operator used in machine learning (but familiar to physicists way before that) to normalize a log-distribution\, turning a vector of (thus\, a function valued in) logits (i.e. additive reals) into a probability distribution. Its name is due to the fact it acts as a 'probabilistic argmax'\, since the modes of a softmax distribution reflects the minima (by an accident of duality) of the function. I will show an attempt to make this statement precise\, by exhibiting the semantics of a 'very linear logic' on the *-autonomous quantale of extended multiplicative reals. In this logic\, additive connectives are also linear\, but are still in the same algebraic relation with the multiplicative ones. I will show how to define quantifiers\, and thus softmax. If time permits\, I'll show a construction of an enriched equipment of relations in which softmax should be characterizable as a Kan lift\, in the same way argmax is characterized as a Kan lift in relations.\n UID:396 END:VEVENT BEGIN:VEVENT DTSTAMP;TZID=Europe/London:20241110T132647 DTSTART;TZID=Europe/London:20240308T150000 DTEND;TZID=Europe/London:20240308T160000 LOCATION:LT209 and Online SUMMARY:TBD DESCRIPTION:Speaker: Paulo Torrens (University of Kent)\nTitle: TBD\n\nThe continuation-passing style (CPS) translation employed within compilers gives rise to a class of target calculi where direct style functions don't exist anymore. While those may be studied using the lambda calculus\, this might not be desired if the language should not be closed under beta-reduction\, such as in the intermediate representation (IR) of Appel's compiler. The purpose of this talk is to introduce ongoing work on the metatheory of Thielecke's CPS-calculus\, a small theory of continuations based on production IRs\, how it relates to actual implementations\, and how this allows us to have a strong theoretical background on the study of name-passing IRs in a similar way that the lambda calculus works as a theoretical foundation for functional programming.\n UID:395 END:VEVENT BEGIN:VEVENT DTSTAMP;TZID=Europe/London:20241110T132647 DTSTART;TZID=Europe/London:20240301T150000 DTEND;TZID=Europe/London:20240301T160000 LOCATION:LT209 and Online SUMMARY:Type-Logical Grammar\, Controlled Substructure\, and Display Calculus DESCRIPTION:Speaker: Wen Kokke (MSP)\nTitle: Type-Logical Grammar\, Controlled Substructure\, and Display Calculus\n\n\n UID:394 END:VEVENT BEGIN:VEVENT DTSTAMP;TZID=Europe/London:20241110T132647 DTSTART;TZID=Europe/London:20240223T150000 DTEND;TZID=Europe/London:20240223T160000 LOCATION:LT209 and Online SUMMARY:Containers for compiler architecture DESCRIPTION:Speaker: Andre Videla (MSP)\nTitle: Containers for compiler architecture\n\nCompiler architecture sucks. It's been left behind by years of software engineering development that have been very successful in developing software past the command-line age. Today\, applications are meant to be responsive\, accessible from a web browser\, enable collaboration\, be multi-platform\, include some generative AI. Some of those ideas are good\, some are bad\, but most compilers do not include any of them. In this presentation\, I aim to showcase how we can revisit the classical "compiler as a function" architecture using containers to bring the idea of compiler architecture to the XXI century.\n UID:393 END:VEVENT BEGIN:VEVENT DTSTAMP;TZID=Europe/London:20241110T132647 DTSTART;TZID=Europe/London:20240216T150000 DTEND;TZID=Europe/London:20240216T160000 LOCATION:LT209 and Online SUMMARY:Making lenses less pointless DESCRIPTION:Speaker: Jules Hedges (MSP)\nTitle: Making lenses less pointless\n\nThis talk contains two ideas. The first is a small trick for programming with lenses in a not-pointfree way\, without using macros or other brittle hacks. The key is something I call a "dialectic"\, which is a value that carries around a delimited continuation with it. The second idea is realising that the central construction of Matteo's "Diegetic Open Games" paper amounts to a monad on the category of lenses that arises as the Kleisli dual of the linear ! comonad in a Dialectica category. By putting these two ideas together we get a shallow DSL for open games\, differentiable programming\, and other applications of categorical cybernetics. This will be a live coding talk using Haskell\, although I think the same ideas should work in any language with first class functions.\n UID:392 END:VEVENT BEGIN:VEVENT DTSTAMP;TZID=Europe/London:20241110T132647 DTSTART;TZID=Europe/London:20240209T150000 DTEND;TZID=Europe/London:20240209T160000 LOCATION:LT209 and Online SUMMARY:Stable domain theory\, Program slicing\, and Automatic Differentiation DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: Stable domain theory\, Program slicing\, and Automatic Differentiation\n\nI'll talk about a connection I think I've discovered between stable domain theory and program slicing by Galois Connections. Stable domain theory considers a refinement of continuous functions between domains that captures the intuitive idea that a "nice" computable functions that produce values must do so by only looking at part of their input\, and that part must be uniquely determined. The same idea turns up in Perera et al.'s formulation of program slicing as Galois connections. I'll try to connect the two via ideas from Automatic Differentiation.\n UID:391 END:VEVENT BEGIN:VEVENT DTSTAMP;TZID=Europe/London:20241110T132647 DTSTART;TZID=Europe/London:20240202T110000 DTEND;TZID=Europe/London:20240202T120000 LOCATION:LT401 and Online SUMMARY:Presheaves on Purpose DESCRIPTION:Speaker: Conor McBride (MSP)\nTitle: Presheaves on Purpose\n\nDependently typed programming languages allow us to define indexed families of datatypes\, e.g.

`Term (n : Nat) : Set`

as
the type of lambda-terms with `n`

variables free. As
declared\, `Term`

is functorial only on the discrete structure
of `Nat`

\, which is to say that it respects equality and
nobody will faint with amazement. But by an outrageous coincidence (which
I learned from Altenkirch\, Hofmann and Streicher)\, such terms can be
acted on by *thinnings* from `n`

to some larger scope
`m`

\, allowing us to carry terms under binders. That is\, we
can demonstrate by honest toil that `Term`

is a functor from
`Thin`

to `Set`

. I dislike honest toil\, and will
show you how to design it away in this and similar situations. To that
end\, I present a universe construction for descriptions of datatypes
indexed over the objects of some category `C`

which\, by
construction\, extend to a functors from `C`

to
`Set`

\, a.k.a. presheaves on `Cop`

.\n
UID:390
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20240126T150000
DTEND;TZID=Europe/London:20240126T160000
LOCATION:LT209 and Online
SUMMARY:Plane Graphs\, (Co-)Operads\, and Pattern Matching
DESCRIPTION:Speaker: Malin Altenmüller (MSP)\nTitle: Plane Graphs\,
(Co-)Operads\, and Pattern Matching\n\nI will present work on open
surface-embedded graphs as representations of string diagrams. The key
feature of these graphs' definition are distinguished boundary vertices
which represent their (outer and inner) boundaries. These special
vertices make it possible to define surface-embeddings of graphs using a
rotation system which specifies an ordering of incident edges at each
vertex. We can then also express graph rewrite rules by their action on
boundary vertices. Additionally\, boundary vertices are a convenient
structure to define planar graphs as operads\, similar to Spivak's Operad
of Wiring Diagrams [1]. I will explain this construction\, as well as a
dual "co-operad" version of it\, and finally the operad-cooperad
interaction which yields a notion of graph pattern matching.\n\n[1]
https://arxiv.org/abs/1305.0297\n
UID:389
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20231204T103000
DTEND;TZID=Europe/London:20231204T170000
LOCATION:University of Strathclyde (MC301)
SUMMARY:Event: CATNIP
DESCRIPTION:The second Categories Network Project (CATNIP) meeting.
UID:388
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20231123T150000
DTEND;TZID=Europe/London:20231123T160000
LOCATION:LT210 and Online
SUMMARY:What do bidirected containers (co-)interpret into?
DESCRIPTION:Speaker: Danel Ahman (University of Ljubljana)\nTitle: What
do bidirected containers (co-)interpret into?\n\nDirected containers are
a neat specialisation of containers that fully faithfully interpret into
comonad structures on the polynomial functor interpretation of the
underlying containers. In terms of shapes and positions\, a directed
container requires the family of positions to form a certain kind of
dependently typed monoid acting on the shapes. In terms of data types\,
directed containers capture structures where every position in a shape
determines a subshape rooted at that position\, e.g.\, positions in a
non-empty list determine sublists rooted at those positions.\n\nIn this
talk I will discuss bidirected containers and what they interpret into.
Bidirected containers specialise directed containers further by asking
the positions to form a certain kind of dependently typed group acting on
the positions. In terms of data types\, this corresponds to every sub
data structure having a position in it that takes one back to the parent
data structure\, i.e.\, data types that behave like zippers. I will also
discuss what we need to seem to ask from comonads to get a similarly
tight correspondence as we have for directed containers. I will end by
wondering whether an analogous story also applies to the cointerpretation
of directed containers as update monads.\n
UID:387
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230929T140000
DTEND;TZID=Europe/London:20230929T150000
LOCATION:LT711 and Online
SUMMARY:An Introduction to Bricks
DESCRIPTION:Speaker: Conor McBride (MSP)\nTitle: An Introduction to
Bricks\n\n\n
UID:386
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20231207T110000
DTEND;TZID=Europe/London:20231207T120000
LOCATION:LT210 and Online
SUMMARY:LabMate --- your faithful and type-safe Matlab assistant
DESCRIPTION:Speaker: Georgi Nakov (MSP)\nTitle: LabMate --- your faithful
and type-safe Matlab assistant\n\nCan you write type-safe Matlab code?
And what can we do to help you write type-safe Matlab?\n\nThis talk is a
report on our progress on LabMate --- an interactive system designed to
improve on current best practices of writing Matlab code. Our key
proposition can be eloquently described as "add types\, all the
types".\n\nI will give a brief tour of the various features in LabMate
and the rationale behind including them. We will also recall the basics
of bidirectional type checking\, what to do to incorporate dimension and
unit checking\, and how to represent matrices with high degree of
generality in our type system. Some of the non-trivial challenges with
Matlab's permissive syntax and elaborating operator overloading will
become apparent in the process.\n\nThis is joint work with Fred and
Conor.\n
UID:384
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20231201T140000
DTEND;TZID=Europe/London:20231201T150000
LOCATION:LT711 and Online
SUMMARY:MSP 101: Non-standard analysis
DESCRIPTION:Speaker: Fredrik Nordvall Forsberg (MSP)\nTitle: MSP 101:
Non-standard analysis\n\nI will give a basic 101-style introduction to
the first-order logic concept of non-standard models. Intuitively\, a
non-standard model of say Peano Arithmetic PA is a model which contains
infinitely large numbers. Yet\, by virtue of being a model of PA\, such a
model still validates all the axioms of PA\, including the induction
axiom schema! It is an interesting and beautiful feature/bug of
first-order classical logic that such models exist.\n
UID:383
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20231122T120000
DTEND;TZID=Europe/London:20231122T170000
LOCATION:University of Strathclyde / Online
SUMMARY:Event: SPLS
DESCRIPTION:
UID:381
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20231117T140000
DTEND;TZID=Europe/London:20231117T150000
LOCATION:LT210 and Online
SUMMARY:Categorical cybernetics for Markov decision processes
DESCRIPTION:Speaker: Riu Rodríguez Sakamoto (MSP)\nTitle: Categorical
cybernetics for Markov decision processes\n\nI will introduce two
ingredients to MSPs 'categorical cybernetics':\n- "open game"-like
categories for backward-filtering problems\n- semiring valuations to
formalize softmax as a *preference* relation (generalizing selection
relations)\n\nThis will allow us to fit Markov decission processes and
certain estimation problems to the existing framework\, clearing our path
towards connecting control and estimation problems.\n
UID:380
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20231103T140000
DTEND;TZID=Europe/London:20231103T150000
LOCATION:LT210 and Online
SUMMARY:Hopf-Frobenius Algebras
DESCRIPTION:Speaker: Joe Collins (MSP)\nTitle: Hopf-Frobenius
Algebras\n\nHopf algebras and Frobenius algebras are two fairly common
algebraic structures. They even look pretty similar if you squint your
eyes - both consist of a monoid/ comonoid pair\, and some algebraic rule
that tells you how they interact. There are a few instances where a
single object in a category has the properties of both a Hopf algebra and
a Frobenius algebra\, called a Hopf-Frobenius algebra. In particular\, ZX
calculus\, a way of modelling quantum circuits using symmetric monoidal
categories\, has this property. Why? And where else does this
occur?\n\nIn this talk\, I will be talking about what a Hopf-Frobenius
algebra is and where it comes from.\n
UID:378
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20231027T140000
DTEND;TZID=Europe/London:20231027T150000
LOCATION:LT210 and Online
SUMMARY:Category Theory ∩ Deep Learning : Where are we\, and where can we
go?
DESCRIPTION:Speaker: Bruno Gavranović (MSP)\nTitle: Category Theory ∩
Deep Learning : Where are we\, and where can we go?\n\nFour years ago I
embarked on my PhD with the goal of exploring the landscape of category
theory\, and its application to artificial neural networks.
Specifically\, I aimed to understand at which level of generality can we
express components of artificial neural networks\, and still meaningfully
capture learning.\n\nIn this talk I will give a progress report on this
goal\, and outline future directions for improvement.\n
UID:377
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20231020T140000
DTEND;TZID=Europe/London:20231020T150000
LOCATION:LT210 and Online
SUMMARY:The double category of adjunctions
DESCRIPTION:Speaker: Ezra Schoen (MSP)\nTitle: The double category of
adjunctions\n\nThere's a particular double category which I've noticed
floating around for a while. The purpose of this talk is to explicitly
describe this double category\, play around in it and see if we can
leverage it to get some `theorems for free'. I'll only be assuming prior
familiarity with 1-categories\, so it should be of general interest. In
fact\, part of the purpose behind this talk is demonstrating that even
for staunch 1-category theorists\, having some higher categories `in the
back pocket' may help in getting a clear picture of what's `really going
on'.\n
UID:376
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20231013T140000
DTEND;TZID=Europe/London:20231013T150000
LOCATION:LT711 and Online
SUMMARY:(Reflexive) Partial Monoids 101
DESCRIPTION:Speaker: Sean Watters (MSP)\nTitle: (Reflexive) Partial
Monoids 101\n\nPartial monoids came up in my work recently\, and I found
them quite interesting. The main goal of this talk is to introduce the
notion into our local sphere of consciousness. After going over the
basics I'll focus mostly on reflexive partial monoids\, the suprisingly
tricky problem of defining exponentiation for them\, and the free
reflexive partial monoid. I'll finish by outlining some remaining
questions that I'm still wondering about.\n
UID:375
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20231006T140000
DTEND;TZID=Europe/London:20231006T150000
LOCATION:Online
SUMMARY:Writing interactive programs using containers
DESCRIPTION:Speaker: Andre Videla (MSP)\nTitle: Writing interactive
programs using containers\n\nContainers and their morphisms provide a
bidirectional structure that matches a lot of programs that are
interactive in nature (databases\, servers\, compilers). In this
presentation I will show how to build such programs using containers\,
container morphisms and their algebra.\n
UID:374
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230922T140000
DTEND;TZID=Europe/London:20230922T150000
LOCATION:LT210 and Online
SUMMARY:Staging by Evaluation
DESCRIPTION:Speaker: Guillaume Allais (MSP)\nTitle: Staging by
Evaluation\n\nI will present an Agda implementation of a simply typed
version of András Kovács' Staged compilation with two-level type
theory.\n\nStarting from an intrinsically typed language mixing static
and dynamic parts using quotes and splices\, we perform a model
construction à la normalisation by evaluation and obtain a staging by
evaluation algorithm.\n
UID:373
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230705T110000
DTEND;TZID=Europe/London:20230705T120000
LOCATION:GH 513 and Online
SUMMARY:A dual adjunction between Ω-automata and Wilke algebras
DESCRIPTION:Speaker: Anton Chernev (University of Groningen)\nTitle: A
dual adjunction between Ω-automata and Wilke algebras\n\nThe notion of
ω-regular language captures the idea of a regular language that consists
of infinite words. The most standard type of automata for ω-regular
languages are called Büchi automata. Ω-automata are another type of
automata for ω-regular languages that\, instead of infinite words\, read
pairs of finite words\, called lassos\, that represent ultimately
periodic words.\nWe study the categorical relationship between Ω-automata
and Wilke algebras – the latter are algebraic structures recognising
ω-regular languages. We present a chain of adjunctions starting from the
category of Ω-automata without initial states and ending with the dual of
the category of quotients of the free Wilke algebra.\nThis is joint work
with Helle Hvid Hansen (University of Groningen) and Clemens Kupke
(University of Strathclyde).\n
UID:372
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230627T160000
DTEND;TZID=Europe/London:20230627T170000
LOCATION:GH 513 and Online
SUMMARY:A Shiny Hammer and Many Nails to Hit – Bidirectional typing is
not only an implementation technique
DESCRIPTION:Speaker: Meven Lennon-Bertrand (University of
Cambridge)\nTitle: A Shiny Hammer and Many Nails to Hit – Bidirectional
typing is not only an implementation technique\n\nIn 2000\, Pierce and
Turner introduced a new technique to perform type inference for ML-like
languages\, whose main idea was to carefully understand the local flow of
information in the algorithm. This technique\, which came to be referred
to as bidirectional typing\, did not come out of a void: similar ideas
had appeared independently in many other contexts. In particular\,
bidirectional typing has been a part of the folklore of dependently typed
languages implementers since the dawn of time.\n\n But even in that
context where it has a long history\, bidirectional typing was for a long
time mostly confined to implementations. Yet\, its type-theoretic
structure turns out to be a very versatile and powerful tool when
studying (dependent) type systems and their meta-theory.\n\n In this
talk\, I will try and give some of my understanding of bidirectional
typing\, how it is rooted in type-checker implementations but is more
than just this\, and how it can be used to make many facets of the
infamously painful meta-theory of dependent type systems a bit less
painful.\n
UID:371
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230630T150000
DTEND;TZID=Europe/London:20230630T160000
LOCATION:GH 513 and Online
SUMMARY:On The Design of a Gradual Dependently Typed Language for
Programming
DESCRIPTION:Speaker: Joey Eremondi (University of Edinburgh)\nTitle: On
The Design of a Gradual Dependently Typed Language for Programming\n\nI
describe a design for gradual dependent types\, a system by which
dependently typed programs can be run when missing parts of types\,
proofs\, or programs. This serves a dual purpose. First\, it reduces the
barrier to entry for dependent types\, making it easier to migrate code
to use dependently typed languages\, and allowing indexed types to be
safely used even when type or proof information is missing. Second\, it
gives dynamic semantics to the typed holes that are already found in
modern languages\, so programs can be safely run when holes are missing\,
providing the programmer with useful information of what terms should
fill the holes. In the talk\, I present a vision for what programming
with gradual dependent types could look like\, along with technical
challenges that arise with it and solutions to some of these
challenges.\n
UID:370
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230616T150000
DTEND;TZID=Europe/London:20230616T160000
LOCATION:LT310 and Online
SUMMARY:Session Types & Imperative Languages & Observations\, Oh My!
DESCRIPTION:Speaker: Jan de Muijnck-Hughes (MSP)\nTitle: Session Types &
Imperative Languages & Observations\, Oh My!\n\nSession Types are a neat
typing discipline to reason both statically and dynamically about program
behaviour. An interesting question is how best we can incorporate session
types into our programming languages and reach the fabled Emerald City of
Type-Driven Validation of Communicating Systems!\n\n Earlier this year\,
I gave a talk at PLUG that discussed the dependently-typed mechanics that
pushed me along the yellow brick road to create Capable\, a featherweight
imperative language that supports Multi-Party Session-Types (MPSTs).
Capable has been mechanised within Idris2 to ensure that including MPSTs
is done honestly as the Good Witch Glinda would appreciate.\n\n In this
talk I intend to step away from the keyboard and take a detour along a
yellow-ish cobbled street to look at some of the theoretical observations
that arise from mechanisation. Specifically\, I will discuss the design
decisions that the Wicked Dependent-Type Checker of the East has
requested I do to ensure unification and execution\, but more importantly
the trade-offs that come with those decisions.\n\n This work is\,
slowly\, getting ready for publication (we do in fact run our
session-typed programs) and I am certain that I don't need to return that
brain\, yet....\n
UID:369
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230621T140000
DTEND;TZID=Europe/London:20230621T150000
LOCATION:MC319 and Online
SUMMARY:Computational Effects in Mathematical Perspective
DESCRIPTION:Speaker: John Power (University of Bath)\nTitle:
Computational Effects in Mathematical Perspective\n\nIn the late 1980's\,
Eugenio Moggi introduced the idea of "monads as notions of computation"\,
the latter more recently called computational effects\, supported by
several impressive examples. He used the definition of monad but did not
make substantial use of mathematics that gives rise to monads. In
category theory\, monads systematically arise from universal algebra. But
universal algebra can also be understood\, from a category theoretic
perspective\, in terms of Lawvere theories\, this fact shedding
considerable light on computational effects\, in particular the
operations that give rise to effects. That observation has been
fundamental to a deep\, further development\, giving rise to the notion
of algebraic effect. I shall try to explain the conceptual line of
thought that gives rise to algebraic effects\, modelled by Lawvere
theories and thence my monads. It was joint work primarily with Gordon
Plotkin but also with others\, notably Martin Hyland.\n
UID:367
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230512T150000
DTEND;TZID=Europe/London:20230512T160000
LOCATION:LT711 and Online
SUMMARY:Just when I thought I was out\, they pull me back in.
DESCRIPTION:Speaker: Ethel Morgan (MSP)\nTitle: Just when I thought I was
out\, they pull me back in.\n\nExperiences from industrial academia &
academic industry.\n
UID:366
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230505T150000
DTEND;TZID=Europe/London:20230505T160000
LOCATION:LT711 and Online
SUMMARY:Modal unification and graph homomorphisms
DESCRIPTION:Speaker: Johannes Marti (Oxford)\nTitle: Modal unification
and graph homomorphisms\n\nThe problem of unifiability in a modal logic L
asks\, whether for a given formula phi there exists a substitution such
that applying the substitution to phi turns it into a theorem of L. For
the many non-transitive modal logics\, most notably the modal logic K\,
it is not known whether this problem is decidable. I present joint work
with Sam van Gool\, where we reformulate unifiability relative to some
modal logics L as a problem about the existence of a graph homomorphism
for some generalised notion of graph that depends on a coalgebra functor
T.\n
UID:365
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230428T150000
DTEND;TZID=Europe/London:20230428T160000
LOCATION:LT711 and Online
SUMMARY:Continuations and co-exponentials
DESCRIPTION:Speaker: Vikraman Choudhury (University of Glasgow)\nTitle:
Continuations and co-exponentials\n\nGrowing up in Indiana\, I learned
about corn-mazes and continuations\, but I found them very confusing\,
often getting lost and struggling to get back on track. Now that I’m
living far away in Scotland\, I find myself reminiscing about my
midwestern roots.\n\n In this talk\, I will present a different
perspective on continuations: just as higher-order functions give you
exponentials\, higher-order continuations give you co-exponentials. On
this motif\, I will develop the theory of co-exponentials and some
applications. I will show how to: (1) combine exponentials and
co-exponentials in the same language without degeneracy\, (2) give a
computational interpretation for bi-intuitionistic logic\, (3) recover
classical control operators and the computational interpretation of
classical logic using Faustian sums\, (4) use co-exponential combinators
to do speculative execution\, backtracking\, and encode effect handlers\,
(5) add co-exponentials to a first-order programming language\, with a
computational interpretation. I will develop these ideas both in syntax
and semantics.\n\n The main idea occurred to me while studying linear
logic and star-autonomous categories\, from Mellies’ micrological study
of negation. The rest of the work builds upon old ideas of Hofmann\,
Streicher\, Reus on models of lambda-mu calculus\, Moggi’s computational
lambda calculus\, Thielecke’s ⊗¬ categories\, Freyd categories of Power\,
Thielecke\, Führmann and others\, and Hasegawa’s contextual calculus.
This work is situated as part of a bigger research programme on trying to
understand the foundations of quantum programming languages\, starting
from first-order reversibility\, instead of linearity.\n
UID:364
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230414T150000
DTEND;TZID=Europe/London:20230414T160000
LOCATION:LT711 and Online
SUMMARY:What are higher categories and groupoids?
DESCRIPTION:Speaker: Thorsten Altenkirch (University of
Nottingham)\nTitle: What are higher categories and
groupoids?\n\nCategories are like drugs: once you get addicted to one\,
your dealer comes up with something stronger and you aquire a new
addiction. This is the games with higher categories.\n\n I want to look
at the definition of higher cats\, actually w,1-cats in HoTT using
semi-simplicial types and the directed replacement of simplicial types.
Also I may discuss the globular approach (which works for higher
groupoids but could also made to work for higher cats) I am wondering how
these are related. This may help to address some open problems.\n
UID:363
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230314T150000
DTEND;TZID=Europe/London:20230314T160000
LOCATION:LT310 and Online
SUMMARY:Systems that model their environments\, and systems that plan.
DESCRIPTION:Speaker: Nathaniel Virgo (Earth-Life Science Institute
(Tokyo))\nTitle: Systems that model their environments\, and systems that
plan.\n\n Consider a system interacting with its environment\, perhaps in
pursuit of some goal. We might want to ask whether the system has a model
of its environment\, especially in POMDP-like cases where the environment
is partially observable and the system must make inferences about the
environment's state in order to pursue its goal.\n\n But where does the
model live in relation to the system? A simple answer is that the
system's state parametrises a probability distribtion over environment
states. This distribution isn't part of the system but is imposed upon it
by an external observer. I will talk about how to model this
observer-dependence via notion of 'interpretation' of a sytem\, in which
a system's internal states are interpreted as being 'about' a hidden
environment state and as being updated using Bayes' theorem. A given
system may have many interpretations\, so that interpretations form a
fibration over systems.\n\n A more interesting case is where a system
uses a model not just to keep track of its environment but to reason
about how to influence it. This is a lot harder to model\, and I will
talk about various pieces of work in progress towards understanding the
relationships between systems\, models and goals\, with an emphasis on a
category-theoretic perspective.\n
UID:362
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230519T150000
DTEND;TZID=Europe/London:20230519T160000
LOCATION:LT711 and Online
SUMMARY:How to be a real™ (C) programmer for beginner type theorists
DESCRIPTION:Speaker: Andre Videla (MSP)\nTitle: How to be a real™ (C)
programmer for beginner type theorists\n\nFeeling impostor syndrome from
writing proof trees yet never executing any programs? Tired of being
marginalized from online communities because you've never dereferenced
raw memory? Finally\, you can become a C-programmer neckbeard with this
one crazy trick without leaving the comfort of your pen&paper. By
extending QTT with pointer operations one can finally achieve their dream
of submitting a patch to the linux kernel and have it be rejected for
naming conventions. At least the program would be correct by construction
since you can inherit all your inductive proofs inside your imperative
program.\n
UID:361
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20241110T132647
DTSTART;TZID=Europe/London:20230609T150000
DTEND;TZID=Europe/London:20230609T160000
LOCATION:LT711 and Online
SUMMARY:Control Flow as a Contour of Data Flow
DESCRIPTION:Speaker: Malin Altenmüller (MSP)\nTitle: Control Flow as a
Contour of Data Flow\n\nI will be talking about some ongoing work on a
compositional graph data structure for encoding control flow information
of a program. At the centre of this definition is the notion of contour
for a given tree-like structure. The notion of contour category was
introduced by Melliès and Zeilberger [1]\, who use it in the context of
representing derivations in context-free grammars as functors. I will
give an overview over their constructions\, and present how we generalise
the notion of contour\, moving to a non-linear\, non-deterministic
version. We use these generalised contours to express control flow
information of a program on top of its abstract syntax tree. I will
discuss how normal flow as well as exceptional program behaviour is
represented in this framework. This is joint work with Dan Ghica.\n\n [1]