BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//MSP//MSP101 v1.0//EN
X-WR-CALNAME: MSP101
X-WR-CALDESC: MSP101 seminar series
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180718T120000
DTEND;TZID=Europe/London:20180718T130000
LOCATION:LT1310
SUMMARY:Finite and Infinite Traces\, Inductively and Coinductively
DESCRIPTION:Speaker: Jurriaan Rot (Radboud University Nijmegen)\nTitle:
Finite and Infinite Traces\, Inductively and Coinductively\n\nIt is a
well-known fact (used e.g. in model checking) that\, on finitely
branching transition systems\, finite trace equivalence coincides with
infinite trace equivalence. I will show how to prove this coinductively\,
which is arguably nicer than the standard inductive proof.\n
UID:177
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180613T110000
DTEND;TZID=Europe/London:20180613T120000
LOCATION:LT1310
SUMMARY:Gillette Fusion: Kits for Hutton's Razor or Type Unsafe and
Scope\n Unsafe Programs and Their Proofs
DESCRIPTION:Speaker: James Chapman (MSP)\nTitle: Gillette Fusion: Kits
for Hutton's Razor or Type Unsafe and Scope\n Unsafe Programs and Their
Proofs\n\nThe paper Type-and-Scope Safe Programs and Their Proofs
abstracts the common type-and-scope safe structure from computations on
lambda-terms that deliver\, e.g.\, renaming\, substitution\, evaluation\,
CPS-transformation\, and printing with a name supply. By exposing this
structure\, we can prove generic simulation and fusion lemmas relating
operations built this way. In this talk I will present this approach but
for simpler setting of Hutton's Razor. This reduces the mathematical
structures involved from relative structures to the ordinary
counterparts.\n
UID:176
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180605T120000
DTEND;TZID=Europe/London:20180605T130000
LOCATION:Cairn Auditorium\, PG G.01\, Postgraduate Centre\, Heriot-Watt University
SUMMARY:Event: SPLS
DESCRIPTION:
UID:175
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180529T130000
DTEND;TZID=Europe/London:20180529T140000
LOCATION:LT1310
SUMMARY:A Coinductive Proof of Policy Iteration Correctness
DESCRIPTION:Speaker: Helle Hvid Hansen (TU Delft)\nTitle: A Coinductive
Proof of Policy Iteration Correctness\n\nThis is the second half of
Helle's talk on a (co)algebraic treatment of Markov Decision Processes.
It focuses on a coinductive explanation of policy improvement using a new
proof principle\, based on Banach's Fixpoint Theorem\, that we call
contraction coinduction.\n
UID:174
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180517T130000
DTEND;TZID=Europe/London:20180517T140000
LOCATION:LT1310
SUMMARY:HoTT for sets
DESCRIPTION:Speaker: Thorsten Altenkirch (Nottingham)\nTitle: HoTT for
sets\n\nBefore getting lost in the realms of higher dimensions we should
see wether we can interpret set-level HoTT. We know how to deal with
functional extensionality and a static universe of propositions (see
Observational Type Theory) but what about a dynamic universe of
propositions\, i.e. one reflecting HProps that also validates
propositional extensionality. I will discuss the problems modelling this
and a possible solution using globular setoids.\n\nThe dynamic prop
corresponds to a subobject classifier in a topos (in particular we get
unique choice) while the static universe corresponds to a quasitopos I am
told.\n
UID:173
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180523T160000
DTEND;TZID=Europe/London:20180523T170000
LOCATION:LT1310
SUMMARY:How Do We Model a Problem Like Mutable State?
DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: How Do We Model a Problem
Like Mutable State?\n\n\n
UID:172
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180516T110000
DTEND;TZID=Europe/London:20180516T120000
LOCATION:LT1310
SUMMARY:Long-Term Values in Markov Decision Processes\, (Co)Algebraically
DESCRIPTION:Speaker: Helle Hvid Hansen (TU Delft)\nTitle: Long-Term
Values in Markov Decision Processes\, (Co)Algebraically\n\nIn this talk\,
we study Markov decision processes (MDPs) with the discounted sums
criterion from the perspective of coalgebra and algebra. Probabilistic
systems\, similar to MDPs but without rewards\, have been extensively
studied\, also coalgebraically\, from the perspective of program
semantics. Here\, we focus on the role of MDPs as models in optimal
planning\, where the reward structure is central. Our main contributions
are: (i) a coinductive explanation of policy improvement using a new
proof principle\, based on Banach's Fixpoint Theorem\, that we call
contraction coinduction\, and (ii) showing that the long-term value
function of a policy can be obtained via a generalized notion of
corecursive algebra\, which takes boundedness into account.\n\nThis is
joint work with Frank Feys (Delft) and Larry Moss (Indiana).\n
UID:171
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180530T110000
DTEND;TZID=Europe/London:20180530T120000
LOCATION:LT1310
SUMMARY:Multi-Dimensional Arrays and their Types
DESCRIPTION:Speaker: Artjoms Šinkarovs and Peter Hancock
(Heriot-Watt)\nTitle: Multi-Dimensional Arrays and their Types\n\nThough
Multi-Dimensional Arrays (MDAs) seem conceptually straightforward\, it's
not easy to come up with a mathematical theory of arrays that can be used
within optimising compilers. We'd like to treat arrays as functions from
indices to values with some domain restrictions. It is desirable that
these domain restrictions are specified in a compact form\, and are
equipped with closed algebraic operations like intersection\, union\,
etc. We are going to consider a few typical models like
hyperrectangulars\, grids and polyhedrons.\n\nWhen typing array
operations\, ideally we'd like to find a balance between tracking all the
shapes of arrays and allowing for generic array operations. This proves
to be tricky\, for reasons we'll explain.\n\nWe will propose\,
tentatively\, an analysis of MDAs in terms of container functors. The aim
is to supply concepts helpful when thinking about MDAs\, e.g. when
designing notations for coding with arrays. Some intriguing gadgetry
shows up.\n
UID:170
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180504T110000
DTEND;TZID=Europe/London:20180504T120000
LOCATION:LT1310
SUMMARY:MSP 101: The Dialectica Interpretation
DESCRIPTION:Speaker: Fredrik Nordvall Forsberg (MSP)\nTitle: MSP 101: The
Dialectica Interpretation\n\nA proof interpretation translates proofs of
one logical system into proofs of another (example: the double-negation
interpretation of classical logic into constructive logic). This often
reveals some information about the original system (e.g. classical logic
is equiconsistent with constructive logic). Gödel's Dialectica
interpretation (named after the journal it was published in) translates
Heyting arithmetic (the constructive theory of the natural numbers\,
including induction) into System T (the quantifier-free theory of the
simply typed lambda calculus with natural numbers) -- quantifier
complexity is traded for higher type complexity. Combining this
translation with (a refined) double negation translation\, one can
extract System T programs from a proof of a forall-exists statement\,
even if this proof is using non-constructive priciples such as Markov's
Principle\, Excluded Middle\, or the Quantifier-Free Axiom of Choice.
I've always found the Dialectica translation mystifying\, so I'll try to
explain the intuition behind it.\n
UID:169
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180419T110000
DTEND;TZID=Europe/London:20180419T120000
LOCATION:LT1310
SUMMARY:Midlands Graduate School Trip Report
DESCRIPTION:Speaker: James Wood (MSP)\nTitle: Midlands Graduate School
Trip Report\n\n\n
UID:168
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180412T110000
DTEND;TZID=Europe/London:20180412T120000
LOCATION:LT1415
SUMMARY:Quotient Inductive-Inductive Types
DESCRIPTION:Speaker: Fredrik Nordvall Forsberg (MSP)\nTitle: Quotient
Inductive-Inductive Types\n\nHigher inductive types (HITs) in Homotopy
Type Theory (HoTT) allow the definition of datatypes which have
constructors for equalities over the defined type. HITs generalise
quotient types and allow to define types which are not sets in the sense
of HoTT (i.e. do not satisfy uniqueness of equality proofs) such as
spheres\, suspensions and the torus. However\, there are also interesting
uses of HITs to define sets\, such as the Cauchy reals\, the partiality
monad\, and the internal\, total syntax of type theory. In each of these
examples we define several types that depend on each other mutually\,
i.e. they are inductive-inductive definitions. We call those HITs
quotient inductive-inductive types (QIITs).\n\nAlthough there has been
recent progress on the general theory of HITs\, there isn't yet a
theoretical foundation of the combination of equality constructors and
induction-induction\, despite having many interesting applications. In
the present paper we present a first step towards a semantic definition
of QIITs. In particular\, we give an initial-algebra semantics and show
that this is equivalent to the section induction principle\, which
justifies the intuitively expected elimination rules.\n
UID:167
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180328T123000
DTEND;TZID=Europe/London:20180328T133000
LOCATION:LT1310
SUMMARY:What is a category\, actually?
DESCRIPTION:Speaker: Thorsten Altenkirch (Nottingham)\nTitle: What is a
category\, actually?\n\nLet us revisit the definition of a category and
define it in a way which has the advantage that we can generalize it to
higher dimensions. Why am I interested in higher categories (or
specifically (\\infty,1)-categories)? I have a few problems in Homotopy
Type Theory which I think can be solved using these beasts: the coherence
problem for type theory in type theory (in the moment I cannot even
define the standard model) and generalizing the Hungarian approach to
Quotient Inductive Inductive Types (QIITs) to Higher Inductive Inductive
Types (HIITs).\n
UID:166
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180321T150000
DTEND;TZID=Europe/London:20180321T160000
LOCATION:LT1415
SUMMARY:Equivariant ZFA and the foundations of nominal techniques
DESCRIPTION:Speaker: Jamie Gabbay (Heriot-Watt)\nTitle: Equivariant ZFA
and the foundations of nominal techniques\n\nThe sets foundations of
nominal techniques are usually taken to be Fraenkel-Mostowski set theory
(which is ZFA + a finite support property). I will argue that in many
situations\, a new foundation which I call Equivariant ZFA (EZFA) may be
a better choice\, because you can do everything in EZFA that you can do
in FM and furthermore EZFA with Choice (EZFAC) is consistent whereas FM
with Choice is not.\n\n* I will define EZFA and how it interacts with
Choice.\n* I will prove that EZFA is *equivalent* to ZFA.\n* I will then
prove that EZFA is *not equivalent* to ZFA.\n* I will explain why I think
EZFA(C) may be useful\, why my last three papers were actually written in
EZFAC\, and finally I will discuss the implications this may have for
mathematical foundations in general.\n\n\nThis talk will be based on the
following paper: http://www.gabbay.org.uk/papers.html#equzfn\n
UID:165
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180214T150000
DTEND;TZID=Europe/London:20180214T160000
LOCATION:LT1310
SUMMARY:MSP 101: Domain Theory
DESCRIPTION:Speaker: Fredrik Nordvall Forsberg (MSP)\nTitle: MSP 101:
Domain Theory\n\nI will give an introduction to Domain Theory\, focusing
on motivation. I hope to cover recursive definitions\, and solving domain
equations using retraction pairs.\n
UID:164
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180208T150000
DTEND;TZID=Europe/London:20180208T160000
LOCATION:LT1212
SUMMARY:Introduction to coalgebra
DESCRIPTION:Speaker: Alexander Kurz (Leicester)\nTitle: Introduction to
coalgebra\n\n\n
UID:163
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180207T150000
DTEND;TZID=Europe/London:20180207T160000
LOCATION:LT1415
SUMMARY:Departmental seminar: From Couplings to Probabilistic Relational
Program Logics
DESCRIPTION:Speaker: Justin Hsu (UCL)\nTitle: From Couplings to
Probabilistic Relational Program Logics\n\nMany program properties are
relational\, comparing the behavior of a program (or even two different
programs) on two different inputs. While researchers have developed
various techniques for verifying such properties for standard\,
deterministic programs\, relational properties for probabilistic programs
have been more challenging. In this talk\, I will survey recent
developments targeting a range of probabilistic relational properties\,
with motivations from privacy\, cryptography\, machine learning. The key
idea is to meld relational program logics with an idea from probability
theory\, called a probabilistic coupling. The logics allow a highly
compositional and surprisingly general style of analysis\, supporting
clean proofs for a broad array of probabilistic relational properties.\n
UID:162
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180406T110000
DTEND;TZID=Europe/London:20180406T120000
LOCATION:LT1310
SUMMARY:Setoids and Quotients
DESCRIPTION:Speaker: James Chapman (MSP)\nTitle: Setoids and
Quotients\n\nIn preparation for Fred's talk about "Quotient
Inductive-Inductive Types" next week I will introduce quotients and
setoids in type theory and some of the issues surrounding them. The use
of setoids is discouraged by many doctors and can lead to a contagious
and incurable condition: relation preservation. Quotients on the other
hand are dangerous if not correctly handled and can lead to unsightly
things appearing where they shouldn't such as inhabitants of the excluded
middle.\n
UID:161
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180314T150000
DTEND;TZID=Europe/London:20180314T160000
LOCATION:LT1310
SUMMARY:Quantum Computing with ZX Calculus
DESCRIPTION:Speaker: Joe Collins (MSP)\nTitle: Quantum Computing with ZX
Calculus\n\nQuantum mechanics is dope\, so it makes sense that making a
computer using the principles of quantum mechanics would also be pretty
sick. However\, the formalism that is used by physicists\, called a
Hilbert space\, is not specialised for this purpose. In particular\, it
is\n1) Difficult to prove properties about programs for quantum
computers\n2) Difficult to see what is these programs are actually
doing\n\nThankfully\, category theory is very cool! Using ZX calculus\,
we can talk about quantum computing in a much clearer manner. I will be
introducing some fundamental quantum mechanics and ZX calculus\, and then
using ZX calculus I will talk about Shor's algorithm.\n
UID:160
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180307T100000
DTEND;TZID=Europe/London:20180307T110000
LOCATION:Level 5\, School of Computing Science\, University of Glasgow
SUMMARY:Event: SPLS
DESCRIPTION:
UID:159
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180221T150000
DTEND;TZID=Europe/London:20180221T160000
LOCATION:LT1310
SUMMARY:A Type-System for describing the Structural Topology of
System-on-a-Chip Architectures
DESCRIPTION:Speaker: Jan de Muijnck-Hughes (Glasgow)\nTitle: A
Type-System for describing the Structural Topology of System-on-a-Chip
Architectures\n\nThe protocols that describe the interactions between IP
Cores on System-on-a-Chip architectures are well-documented. These
protocols described not only the structural properties of the physical
interfaces but also the behaviour of the emanating signals. However\,
there is a disconnect between the design of SoC architectures\, their
formal description\, and the verification of their implementation in
known hardware description languages.\n\nWithin the Border Patrol project
we are investigating how to capture and reason about the structural and
behavioural properties of SoC architectures using state-of-the-art
advances in programming language research. Namely\, we are investigating
using dependent types and session types for the description of hardware
communication.\n\nIn this talk I will discuss my work in designing a
linked family of languages that captures and reasons about the
topological structure of a System-on-a-Chip. These languages provide
correct-by-construction guarantees over the interaction protocols
themselves\; the adherence of a component that connects using said
protocols\; and the validity of the specified connections. These
guarantees are provided through abuse of indexed monads to reason about
resource usage\; and general (ab)use of dependent types as presented in
Idris.\n\nI will not cover all aspects of the languages but will
concentrate my talk detailing the underlying theories that facilitate the
correct-by-construction guarantees.\n
UID:158
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180309T160000
DTEND;TZID=Europe/London:20180309T170000
LOCATION:LT1310
SUMMARY:MSP 101: Kan extensions
DESCRIPTION:Speaker: Alasdair Lambert and Ben Price (MSP)\nTitle: MSP
101: Kan extensions\n\n\n
UID:157
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180207T150000
DTEND;TZID=Europe/London:20180207T160000
LOCATION:LT1310
SUMMARY:MSP 101: The adjoint functor theorem
DESCRIPTION:Speaker: Fredrik Nordvall Forsberg (MSP)\nTitle: MSP 101: The
adjoint functor theorem\n\nAdjoint functors arise everywhere\, but how do
we find them? It is a fun exercise to prove that right adjoints preserve
limits\, and\, dually\, that left adjoints preserve colimits. An adjoint
functor theorem is a statement that (under certain conditions) the
converse holds: a functor which preserves limits is a right adjoint. I
will discuss the General Adjoint Functor Theorem\, and why Peter
Johnstone considers it fundamentally useless.\n
UID:155
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180131T150000
DTEND;TZID=Europe/London:20180131T160000
LOCATION:LT1310
SUMMARY:Reflections on the PhD process
DESCRIPTION:Speaker: Kevin Dunne (MSP)\nTitle: Reflections on the PhD
process\n\n\n
UID:154
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180124T150000
DTEND;TZID=Europe/London:20180124T160000
LOCATION:LT1310
SUMMARY:Coinduction and the Companion
DESCRIPTION:Speaker: Jurriaan Rot (Radboud University Nijmegen)\nTitle:
Coinduction and the Companion\n\nThe coinductive proof method can be
enhanced by several techniques\, often referred to as up-to-techniques. I
will talk about the basic theory of coinduction-up-to\, and a little
about the more recent notion of companion. This companion is the largest
valid up-to technique for a given predicate\, and gives a nice way of
working with coinduction up-to.\n
UID:153
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20180116T160000
DTEND;TZID=Europe/London:20180116T170000
LOCATION:LT1310
SUMMARY:Event: MSP101 Planning session
DESCRIPTION:
UID:152
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20171208T160000
DTEND;TZID=Europe/London:20171208T170000
LOCATION:LT1310
SUMMARY:Dijkstra Monads
DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: Dijkstra Monads\n\nOne monad
to the tune of another.\n
UID:151
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20171027T160000
DTEND;TZID=Europe/London:20171027T170000
LOCATION:LT1310
SUMMARY:Size-Matters in the Modal mu-Calculus
DESCRIPTION:Speaker: Johannes Marti (Universität Bremen)\nTitle:
Size-Matters in the Modal mu-Calculus\n\nI talk about three methods for
measuring the size of formulas in the modal mu-calculus and explore how
the choice between them influences the complexity of computations on
formulas. Especially\, I focus on the guarded transformation\, which is a
simple syntactic transformation on formulas that is commonly assumed to
be polynomial but has recently been shown to require exponential
time.\n\nI will complain about the mess in the literature and present two
of our (Clemens\, Yde and me) own preliminary results:\n\n1) There is a
polynomial guarded transformation if we measure the input formula in the
number of its subformulas and measure the output formula in the size of
its closure.\n\n2) If there is a polynomial guarded transformation where
we measure the input formula in the size of its closure then there is a
polynomial algorithm for solving parity games. Hence finding such a
transformation is at least as hard as solving parity games\, which is
commonly believed to be quite hard.\n\nWe employ an automata-theoretic
approach that relates the different measures for the size of a formula to
different constraints on the transition structure of an automaton
corresponding to the formula.\n\nThis is a very technical talk but there
will be many pictures!\n
UID:150
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20171011T120000
DTEND;TZID=Europe/London:20171011T130000
LOCATION:Informatics Forum\, Edinburgh
SUMMARY:Event: SPLS
DESCRIPTION:
UID:149
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170922T160000
DTEND;TZID=Europe/London:20170922T170000
LOCATION:LT1310
SUMMARY:Bidirectional Martin-Löf 1971
DESCRIPTION:Speaker: Conor McBride (MSP)\nTitle: Bidirectional Martin-Löf
1971\n\nPer Martin-Löf's 1971 Theory of Types is the ancestor of the type
systems used today in Agda\, Coq\, Idris\, NuPRL\, and many other
variations on the theme of dependent types. Its principal virtue is its
simplicity: it has very few moving parts (but they move quite a lot). Its
well known principal vice is its inconsistency: you can write a looping
program inhabiting any type (thus 'proving' any proposition). I'll be
talking about the design principles for constructing dependent type
systems which are bidirectional -- clearly split into a type checking
part and a type synthesis part. By following these principles\, it gets
easier to establish good safety properties of these systems. In
particular\, I'll sketch how to keep type safety ("well typed programs
don't go wrong") separate from normalization ("all computations
terminate"). Martin-Löf's 1971\, reformulated bidirectionally\, makes
a good example\, because it's small and type-safe\, but not
normalizing.\n
UID:148
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170929T160000
DTEND;TZID=Europe/London:20170929T170000
LOCATION:LT1310
SUMMARY:Worlds
DESCRIPTION:Speaker: Ben Price (MSP)\nTitle: Worlds\n\nBuilding on last
week's introduction to Martin-Löf 1971\, we describe a toy type theory
which not only accounts for what type terms have\, but also where they
live. This extra information can be interpreted as where (physically)
data lives\, at what phase (typechecking vs runtime) it exists\, when it
exists\, or who has access to the data.\n\nIn return for caring about
these "worlds" describing where data lives\, we get applications to
distributed computing and erasure for efficient code generation\, with
future work to consider productivity and security.\n
UID:147
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20171006T160000
DTEND;TZID=Europe/London:20171006T170000
LOCATION:LT1310
SUMMARY:Tetration
DESCRIPTION:Speaker: Peter Hancock \nTitle: Tetration\n\nIn ghci\, you
can write something like `let two f = f . f in two two two two (+1)
0` and it will print "65536". If you write something like `let two f = f . f \; four = two . two in four ($
two) id (+1) 0` \n it will print "Occurs check: cannot construct the
infinite type: a ~ a -> a".\n\nCan haskell not count to four?(*)\n\nThe
topic is the compact representation of unfeasibly large numbers using a
pure (Glaswegian?) universe. Some excursions into the hinterland of the
topic are likely.\n\nBy the way\, tetration is the function m n |-> n ^
.. ^ n with m n's.\n\n(*) No doubt mad haskell mambo or pragma exists
that will trick it into counting up to four. I will reward the most
amusing/revolting demonstration with a large (reasonably priced) malt
whisky.\n
UID:146
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20171013T160000
DTEND;TZID=Europe/London:20171013T170000
LOCATION:LT1310
SUMMARY:Coalgebraic Learning
DESCRIPTION:Speaker: Simone Barlocco (MSP)\nTitle: Coalgebraic
Learning\n\nAutomata learning is a well known technique to infer a finite
state machine from a set of observations. One important algorithm for
automata learning is the L* algorithm by Dana Angluin. In this 101 I will
present a new perspective on L* using ideas from coalgebra and modal
logic. After a brief recap of how L* works\, I will describe a
generalisation of the L* algorithm to the coalgebraic level. I will
conclude my talk with two concrete instances of the general framework:
the learning of Mealy machines and of bisimulation quotients of
probabilistic transition systems. Joint work with Clemens Kupke.\n
UID:145
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20171103T160000
DTEND;TZID=Europe/London:20171103T170000
LOCATION:LT1310
SUMMARY:Measuring the sizes of trees
DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: Measuring the sizes of
trees\n\nI'll talk about a way of measuring the sizes of trees using
weighted tree automata\, in a compositional way that works well with
pattern matching. This is based on some work by Georg Moser and Martin
Hofmann.\n
UID:144
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20171117T160000
DTEND;TZID=Europe/London:20171117T170000
LOCATION:LT1310
SUMMARY:Deep Learning
DESCRIPTION:Speaker: Ross Duncan (MSP)\nTitle: Deep Learning\n\nI'll
explain the first concepts of Deep Learning. This is an advert for a
reading group on the topic which will run over the next few weeks.\n
UID:143
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20171110T160000
DTEND;TZID=Europe/London:20171110T170000
LOCATION:LT1310
SUMMARY:Infinite Iteration of Games
DESCRIPTION:Speaker: Alasdair Lambert (MSP)\nTitle: Infinite Iteration of
Games\n\nMy talk will be based on our recent paper "A Compositional
Treatment of Iterated Open Games". In this paper we introduce a new
operator on open games to capture the concept of subgame perfect
equilibrium as well as providing final coalgebra semantics of infinite
games.\n
UID:141
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20171201T160000
DTEND;TZID=Europe/London:20171201T170000
LOCATION:LT1310
SUMMARY:MSP 101: Hereditary substitution
DESCRIPTION:Speaker: Conor McBride (MSP)\nTitle: MSP 101: Hereditary
substitution\n\n\n
UID:138
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20171206T130000
DTEND;TZID=Europe/London:20171206T140000
LOCATION:LT1415
SUMMARY:The Power of Parameterization in Coinductive Proof
DESCRIPTION:Speaker: Chung-Kil Hur (Seoul National University)\nTitle:
The Power of Parameterization in Coinductive Proof\n\nIn this talk\, I
will present a simple yet powerful principle for coinductive reasoning\,
which we call "parameterized coinduction". More specifically\, it is as
simple as the Knaster-Tarski theorem without requiring any syntactic
checking\, yet as powerful as Coq's syntactic guarded coinduction
supporting incremental reasoning. As an important consequence\,
parameterized coinduction can easily support complex nested
induction-coinduction. \n\nWe also implemented the parameterized
coinduction as the Coq library called "paco"\, which can be found
at:\n\nhttp://plv.mpi-sws.org/paco\n\nThis is joint work with Georg
Neis\, Derek Dreyer and Viktor Vafeiadis\, and was presented at POPL'13.
\n
UID:137
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170914T114000
DTEND;TZID=Europe/London:20170914T124000
LOCATION:LT1310
SUMMARY:Event: MSP101 Planning session
DESCRIPTION:
UID:136
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170911T140000
DTEND;TZID=Europe/London:20170911T150000
LOCATION:LT1101 (Board room)
SUMMARY:Adding Cubes to Agda
DESCRIPTION:Speaker: Andrea Vezzosi (Chalmers)\nTitle: Adding Cubes to
Agda\n\nCubical Type Theory (CTT) provides an extension of Martin-Löf
Type Theory (MLTT) where we can interpret the univalence axiom while
preserving the canonicity property\, i.e. every closed term actually
computes to a value. The typing and equality rules of CTT come as a
fairly well-behaved extension of the ones of MLTT and the denotational
model and prototype implementation help clarifying the system
further.\n\nGiven the above it felt reasonable to introduce the features
of CTT into a more mature proof assistant like Agda\, and this talk
reports the status of this endeavour. In short:\n\n* The univalence axiom
is proven as a theorem and we successfully tested its computational
behavior on small examples.\n* `comp` computes for any
parametrized data or record types\, including coinductive ones\, but it
is stuck for inductive families.\n* The interaction of the path type and
copatterns gives extensionality principles for coinductive records.\n*
The interval `I` is an actual type\, we also have restriction
types `A[&phi&mapsto\; u]` and types for partial elements
`Partial &phiA`. Their sort makes sure `comp` does not
apply to them.\n\nExamples are collected at
https://github.com/Saizan/cubical-demo.\n
UID:135
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170906T140000
DTEND;TZID=Europe/London:20170906T150000
LOCATION:LT1310
SUMMARY:Binding and Substitution in String Diagrams
DESCRIPTION:Speaker: Ross Duncan (MSP)\nTitle: Binding and Substitution
in String Diagrams\n\nIn the categorical semantics of (e.g.) the simply
typed lambda calculus substitution of a variable by a term is achieved by
composing morphisms. What is the equivalent notion in diagrammatic
languages? What even is a "variable" in this context? I'll sketch some
(pretty) rough ideas for the beginnings of a “functional language” of
diagrams including substitution\, binding\, and pattern matching. It
turns out to all be about operads and co-operads.\n
UID:134
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170710T100000
DTEND;TZID=Europe/London:20170710T110000
LOCATION:LT1415
SUMMARY:Event: Open Games Workshop
DESCRIPTION:
UID:133
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170705T140000
DTEND;TZID=Europe/London:20170705T150000
LOCATION:LT1415
SUMMARY:Some enumerative\, topological\, and algebraic aspects of linear
lambda calculus
DESCRIPTION:Speaker: Noam Zeilberger (Birmingham)\nTitle: Some
enumerative\, topological\, and algebraic aspects of linear lambda
calculus\n\nEnumeration of graphs on surfaces (or "maps") is an active
topic of research in combinatorics\, with links to wide-ranging domains
such as algebraic geometry\, knot theory\, and mathematical physics. In
the last few years\, it has also been found that map enumeration is
related to the combinatorics of lambda calculus\, with various well-known
families of maps in 1-to-1 correspondence with various natural families
of linear lambda terms. In the talk I will begin by giving a brief survey
of these enumerative connections\, then use those to motivate a closer
look at the surprisingly rich topological and algebraic properties of
linear lambda calculus.\n
UID:132
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170615T140000
DTEND;TZID=Europe/London:20170615T150000
LOCATION:LT1310
SUMMARY:Informal introduction to knot theory and the unknotting problem
DESCRIPTION:Speaker: Stuart Gale (MSP)\nTitle: Informal introduction to
knot theory and the unknotting problem\n\nThis is an informal talk on the
interesting properties I've found when playing with the unknotting
problem (knot simplification moves that help to establish whether any
given knot is a loop in complicated disguise\, or something really
knotted).\n\nI'll discuss the syntax that I've used for annotating knots
that leads to a(n almost) syntax based method for unknotting\, but that
hints further at unknotting in a more interesting way by using an
unintentional property of the syntax.\n\nI'll present some examples of
the problems with representing knots and how the syntax and reduction
rules help\, in my opinion\, to make unknotting more tangible.\n
UID:131
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170629T140000
DTEND;TZID=Europe/London:20170629T150000
LOCATION:LT1310
SUMMARY:Syntax and semantics of Quantitative Type Theory
DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: Syntax and semantics of
Quantitative Type Theory\n\nAt last year's WadlerFest celebration\, Conor
presented a dependent type theory where variables are tagged with
information about how they are used. Variable usage tagging has been
developed in the non dependent setting\, starting with Girard's Linear
Logic\, and culminating with recent work in contextual effects\,
coeffects\, and quantitative type theories. The subtlety with dependent
types lies in how to account for the difference between usage in types
and terms. Conor's system handles this by treating usage in types as a
"zero" usage\, so that it doesn't affect the usage in terms. This is a
departure from previous "linear" type theories that maintains a strict
separation between usage controlled information\, which types cannot
depend on\, and unrestricted information\, which types can depend
on.\n\nConor presented a syntax and typing rules for the system\, as well
as an erasure property that exploits the difference between "not used"
and "used"\, but doesn't do anything with the finer usage information
available. I'll present a collection of models for the system that fully
exploit the usage information. This will give interpretations of type
theory in resource constrained computational models\, Geometry of
Interaction models\, and imperative models. To maintain order\, I will
gather all these notions of model under a new concept of "Quantitative
Category with Families"\, a generalisation of the standard "Category with
Families" class of models of dependent types.\n
UID:130
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170608T140000
DTEND;TZID=Europe/London:20170608T150000
LOCATION:LT1310
SUMMARY:TYPES 2017 Trip report
DESCRIPTION:Speaker: Fredrik Nordvall Forsberg (MSP)\nTitle: TYPES 2017
Trip report\n\nI'll tell you about the most interesting talks\, ideas and
gossip that came out of the TYPES conference in BudaPest last week.\n
UID:129
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170727T140000
DTEND;TZID=Europe/London:20170727T150000
LOCATION:LT1415
SUMMARY:The Rise and Fall of Cooperative Communities
DESCRIPTION:Speaker: Matteo Cavaliere (Edinburgh)\nTitle: The Rise and
Fall of Cooperative Communities\n\nSocial\, biological and economic
networks grow and decline with recurrent fragmentation and re-formation\,
often explained in terms of external perturbations. I will present a
model of dynamical networks and evolutionary game theory that explains
these phenomena as consequence of imitation and endogenous conflicts
between "cooperators" and "cheaters". Cooperators promote well-connected
prosperous (but fragile) networks and cheaters cause the network to
fragment and lose its prosperity. Once the network is fragmented it can
be reconstructed by a new invasion of cooperators\, leading to recurrent
cycles of formation and fragmentation observed\, for instance\, in
bacterial communities and socio-economic networks. In the last part of
the talk\, I will briefly introduce my current works on the role of
individual decision-making in cooperative communities and the possibility
of synthetic biology to address these ideas in microbial
communities.\n\nReferences\n\nM. Cavaliere\, S. Sedwards\, C.E. Tarnita\,
M.A. Nowak\, A. Csikasz-Nagy.\nProsperity is Associated with Instability
in Dynamical Networks.\nJournal of Theoretical Biology\, 299\,
2012.\n\nPlasticity Facilitates Sustainable Growth in the Commons.\nM.
Cavaliere\, J.F. Poyatos.\nJournal of the Royal Society Interface\, 10\,
2013.\n\nEco-Evolutionary Feedbacks can Rescue Cooperation in Microbial
Populations.\nC. Moreno-Fenoll\, M. Cavaliere\, E. Martinez-Garcia\, J.F.
Poyatos.\nScientific Reports\, 7\, 2017.\n
UID:128
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170601T140000
DTEND;TZID=Europe/London:20170601T150000
LOCATION:LT1310
SUMMARY:Optimal nondeterminism: explaining the Kameda-Weiner algorithm
DESCRIPTION:Speaker: Rob Myers \nTitle: Optimal nondeterminism:
explaining the Kameda-Weiner algorithm\n\nThe Kameda-Weiner algorithm
takes a machine (nondeterministic finite automaton) as input\, and
provides an optimal machine (state-minimal nondeterministic finite
automaton) as output. In this talk I will discuss work which provides a
clear explanation of it\, by translating the various syntactic constructs
into more meaningful order-theoretic ones\, and then composing them
together to prove correctness.\n
UID:127
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170525T110000
DTEND;TZID=Europe/London:20170525T120000
LOCATION:LT1310
SUMMARY:Learning via Coalgebraic Logic
DESCRIPTION:Speaker: Clemens Kupke (MSP)\nTitle: Learning via Coalgebraic
Logic\n\nA key result in computational learning theory is Dana Angluin's
L* algorithm that describes how to learn a regular language\, or a
deterministic finite automaton (DFA)\, using membership and equivalence
queries. In my talk I will present a generalisation of this algorithm
using ideas from coalgebra and modal logic -- please note\, however\,
that prior knowledge of these topics will not be required.\n\nIn the
first part of my talk I will recall how the L* algorithm works and
establish a link to the notion of a filtration from modal logic.
Furthermore I will provide a brief introduction to coalgebraic modal
logic. In the second part of my talk I will present a generalisation of
Angluin's original algorithm from DFAs to coalgebras for an arbitrary
finitary set functor T in the following sense: given a (possibly
infinite) pointed T-coalgebra that we assume to be regular (i.e. having
an equivalent finite representation) we can learn its finite
representation by (i) asking "logical queries" (corresponding to
membership queries) and (ii) making conjectures to which a teacher has to
reply with a counterexample (equivalence queries). This covers (known
variants of) the original L* algorithm and algorithms for learning Mealy
and Moore machines. Other examples are infinite streams\, trees and
bisimulation quotients of various types of transition systems.\n\nJoint
work with Simone Barlocco.\n
UID:126
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170518T150000
DTEND;TZID=Europe/London:20170518T160000
LOCATION:LT1310
SUMMARY:The joy of QIITs
DESCRIPTION:Speaker: Thorsten Altenkirch (Nottingham)\nTitle: The joy of
QIITs\n\nQuotient inductive inductive types (QIITS) are set-truncated
mutually defined higher inductive types. I am going to discuss two
applications of QIITs:\n\n1. define an internal syntax of Type Theory
without reference to untyped preterms;\n2. define a version of the
partiality monad that doesn't require countable choice.\n\nOn the one
hand I think that these applications are interesting because they
represent applications of HoTT which have nothing to do with homotopy
theory\; on the other hand they are clearly not very higher order (in the
sense of truncation levels) but can be defined in the set-truncated
fragment of HoTT. Hence my question: what are interesting applications of
higher types which are not directly related to synthetic homotopy
theory?\n\nThis talk is based on joint work with Paolo Capriotti\, Nils
Anders Danielsoon\, Gabe Dijkstra\, Ambrus Kaposi and Nicolai Kraus.\n
UID:125
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170420T140000
DTEND;TZID=Europe/London:20170420T150000
LOCATION:LT1310
SUMMARY:Modular Datalog
DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: Modular Datalog\n\n\n
UID:124
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170504T140000
DTEND;TZID=Europe/London:20170504T150000
LOCATION:LT1310
SUMMARY:MSP 101: Differential Operators
DESCRIPTION:Speaker: Conor McBride (MSP)\nTitle: MSP 101: Differential
Operators\n\nA traditional source of complaint from CS undergraduates
(especially in the USA\, but in other places\, too) is that they are made
to learn too much standard issue mathematics with little apparent
relevance to computation. Differential calculus (with its usual
presentational focus on physical systems) is often picked upon as the
archetype. What we see in action is the fragile male ego: they are not so
quick to complain about the unimportance of things they do not find
difficult. All of which makes more delicious the irony that differential
operators have a key role to play in understanding discrete structures\,
such as automata\, datatypes\, execution stacks\, and plenty more.\n\nThe
basic idea is as follows: to put your finger over any single K in the
pair of words BREKEKEKEX KOAXKOAX \n you must choose either to put your
finger over a single K in BREKEKEKEX and pair with KOAXKOAX intact\, or
to leave BREKEKEKEX intact and cover a K in KOAXKOAX. You have just
followed Leibniz's rule for differentiating a product (with respect to
K)\, and computed a one-hole context for a K in a data
structure.\n\nNewton\, of course\, would point out that such derivatives
arise as the limit of a divided difference\, a concept worthy of study in
more generality. I would point out that divided differences are often
definable\, even in situtations when neither division nor difference
makes much apparent sense. Notably\, Brzozowski's derivative for regular
languages is a divided difference (even though it is not Leibniz's
derivative).\n\nI'll work mainly with containers (which look a lot like
power series) but make sure there are plenty of concrete examples. In
practice\, it becomes rather useful to compute derivatives by pattern
matching on types\, which is especially funny as symbolic differentiation
is the first example in the literature of computing anything by pattern
matching at all.\n
UID:123
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170405T100000
DTEND;TZID=Europe/London:20170405T110000
LOCATION:Strathclyde\, room LT1415
SUMMARY:Event: CLAP
DESCRIPTION:
UID:122
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170410T090000
DTEND;TZID=Europe/London:20170410T100000
LOCATION:Strathclyde\, Room MC301 (McCance Building)
SUMMARY:Event: ALCOP2017
DESCRIPTION:
UID:121
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170222T150000
DTEND;TZID=Europe/London:20170222T160000
LOCATION:LT1415
SUMMARY:Departmental seminar: An introduction to Blockchains
DESCRIPTION:Speaker: Andrea Bracciali (Stirling)\nTitle: An introduction
to Blockchains\n\nBlockchains\, i.e. decentralised\, distributed data
structures which can also carry executable code for a non-standard
execution environment\, introduce new models of computation.
Decentralised\, here\, means\, informally speaking\, "without central
control"\, e.g. a currency without a (central) bank\, but much more.
Blockchains support the recently introduced virtual currencies\, a la
Bitcoin\, and a new class of decentralised applications\, including smart
contracts. In this talk we will introduce the main aspects of a
blockchain\, with particular reference to the Bitcoin blockchain as a
paradigmatic case of such a new model of computation\, and also touching
on smart contracts. No previous knowledge of bitcoin/blockchain required
for this introductory talk.\n
UID:120
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170215T130000
DTEND;TZID=Europe/London:20170215T140000
LOCATION:LT1415
SUMMARY:Departmental seminar: Semantics for probabilistic programming
DESCRIPTION:Speaker: Chris Heunen (Edinburgh)\nTitle: Semantics for
probabilistic programming\n\nStatistical models in e.g. machine learning
are traditionally expressed in some sort of flow charts. Writing
sophisticated models succinctly is much easier in a fully fledged
programming language. The programmer can then rely on generic inference
algorithms instead of having to craft one for each model. Several such
higher-order functional probabilistic programming languages exist\, but
their semantics\, and hence correctness\, are not clear. The problem is
that the standard semantics of probability theory\, given by measurable
spaces\, does not support function types. I will describe how to get
around this.\n
UID:119
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170206T140000
DTEND;TZID=Europe/London:20170206T150000
LOCATION:LT1415
SUMMARY:On the expressive power of user-defined effects: effect
handlers\, monadic reflection\, delimited control without
answer-type-modification
DESCRIPTION:Speaker: Ohad Kammar (Oxford)\nTitle: On the expressive power
of user-defined effects: effect handlers\, monadic reflection\, delimited
control without answer-type-modification\n\nWe compare the expressive
power of three programming abstractions for user-defined computational
effects: Bauer and Pretnar's effect handlers\, Filinski's monadic
reflection\, and delimited control. This comparison allows a precise
discussion about the relative merits of each programming
abstraction.\n\nWe present three calculi\, one per abstraction\,
extending Levy's call-by-push-value. These comprise syntax\, operational
semantics\, a natural type-and-effect system\, and\, for handlers and
reflection\, a set-theoretic denotational semantics. We establish their
basic meta-theoretic properties: adequacy\, soundness\, and strong
normalisation. Using Felleisen's notion of a macro translation\, we show
that these abstractions can macro-express each other\, and show which
translations preserve typeability. We use the adequate finitary
set-theoretic denotational semantics for the monadic calculus to show
that effect handlers cannot be macro-expressed while preserving
typeability either by monadic reflection or by delimited control. We
supplement our development with a mechanised Abella
formalisation.\n\nJoint work with Yannick Forster\, Sam Lindley\, and
Matija Pretnar.\n
UID:118
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170427T140000
DTEND;TZID=Europe/London:20170427T150000
LOCATION:LT1310
SUMMARY:What I\, Dunne\, done in my PhD
DESCRIPTION:Speaker: Kevin Dunne (MSP)\nTitle: What I\, Dunne\, done in
my PhD\n\n\n
UID:117
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170330T140000
DTEND;TZID=Europe/London:20170330T150000
LOCATION:LT1310
SUMMARY:Cubical adventures in Connecticut
DESCRIPTION:Speaker: Fredrik Nordvall Forsberg (MSP)\nTitle: Cubical
adventures in Connecticut\n\nI'll report on my attempts to design a
cubical type theory together with Dan Licata and Ed Morehouse during my
visit to Wesleyan University\, Middletown\, Connecticut. We had something
which seemed quite promising\, but that falls apart just short of the
finish line\; I'll tell you about it in the hope of miraculous rescue
from the audience. However\, I'll start from basics so that everyone has
a chance to join in in the fun. Mentions of Donald Trump will be kept to
a minimum.\n
UID:116
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170323T140000
DTEND;TZID=Europe/London:20170323T150000
LOCATION:LT1310
SUMMARY:Blockchain discussion
DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: Blockchain discussion\n\n\n
UID:115
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170316T140000
DTEND;TZID=Europe/London:20170316T150000
LOCATION:LT1310
SUMMARY:MSP 101: Operational and Denotational Semantics for PCF
DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: MSP 101: Operational and
Denotational Semantics for PCF\n\nPCF is the prototypical functional
programming language\, with two data types (naturals and booleans)\,
lambda-abstraction and recursion. PCF was introduced by Gordon Plotkin in
his seminal "LCF Considered as a Programming Language" paper from 1977.
Despite PCF's simplicity\, its semantics is theoretically interesting. I
will introduce PCF\, its operational semantics\, the "standard"
domain-theoretic denotational semantics and show that the two agree on
closed programs. Finally\, I will discuss observational equivalence for
PCF and show that the denotational semantics fails to be "fully
abstract".\n
UID:114
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170309T140000
DTEND;TZID=Europe/London:20170309T150000
LOCATION:LT1310
SUMMARY:MSP 101: Indexed Containers/Interaction Structures
DESCRIPTION:Speaker: Conor McBride (MSP)\nTitle: MSP 101: Indexed
Containers/Interaction Structures\n\n\n
UID:113
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170302T140000
DTEND;TZID=Europe/London:20170302T150000
LOCATION:LT1310
SUMMARY:MSP 101: Separation Logic and Hoare Logic
DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: MSP 101: Separation Logic
and Hoare Logic\n\nHoare Logic is a logic for proving properties of
programs of the form: if the initial state satisfies a precondition\,
then the final state satisfies a postcondition. Hoare logic proofs are
structured around the structure of the program itself\, making the system
a compositional one for reasoning about pieces of programs. I'll
introduce Hoare Logic for a little imperative language with WHILE loops.
I'll then motivate Separation Logic\, which enriches Hoare Logic with a
Frame Rule for local reasoning. \n
UID:112
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170223T140000
DTEND;TZID=Europe/London:20170223T150000
LOCATION:LT1415
SUMMARY:MSP 101: Blockchain
DESCRIPTION:Speaker: James Chapman (MSP)\nTitle: MSP 101: Blockchain\n\nI
will try to follow on from yesterday's introduction by getting to nitty
gritty of bitcoin/blockchain. I won't assume attendance of the seminar
but will try not to repeat it!\n
UID:111
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170216T140000
DTEND;TZID=Europe/London:20170216T150000
LOCATION:LT1310
SUMMARY:MSP 101: Automata on infinite words
DESCRIPTION:Speaker: Clemens Kupke (MSP)\nTitle: MSP 101: Automata on
infinite words\n\nIn this 101 I plan to discuss omega-automata\, i.e.\,
finite automata that operate on infinite words/streams. These automata
form an important tool for the specification and verification of the
ongoing\, possibly infinite behaviour of a system. In my talk I will
provide the standard definition(s) of omega-automata and highlight what
makes omega-automata difficult from a coalgebraic perspective. Finally\,
I am going to discuss the work by Ciancia & Venema that provides a first
coalgebraic representation of a particular type of omega-automata\,
so-called Muller automata.\n
UID:110
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170209T140000
DTEND;TZID=Europe/London:20170209T150000
LOCATION:LT1310
SUMMARY:MSP 101: Automata learning
DESCRIPTION:Speaker: Simone Barlocco (MSP)\nTitle: MSP 101: Automata
learning\n\nAutomata learning is a well known technique to infer a finite
state machine from a set of observations. One important algorithm for
automata learning is the L* algorithm by Dana Angluin. In this 101\, I
will explain how the L* algorithm works via an example. Afterwards\, I
will discuss the ingredients of the algorithm both in the standard
framework by Angluin and in a recently developed categorical/coalgebraic
framework by Jacobs & Silva. Lastly\, I plan to outline the proof of the
minimality of the automaton that is built by the learning algorithm.\n
UID:109
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170202T140000
DTEND;TZID=Europe/London:20170202T150000
LOCATION:LT1310
SUMMARY:MSP 101: First-order logic
DESCRIPTION:Speaker: Johannes Marti (MSP)\nTitle: MSP 101: First-order
logic\n\nIn this 101 I outline the syntax and semantics of classical
first order predicate logic. I try to also mention some of the
characteristic properties of first order logic such as compactness\, the
Löwenheim-Skolem theorem or locality properties in finite model theory.\n
UID:108
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170126T140000
DTEND;TZID=Europe/London:20170126T150000
LOCATION:LT1310
SUMMARY:La Vie Parisienne: POPL trip report
DESCRIPTION:Speaker: Conor McBride\, James Chapman\, and Bob Atkey
(MSP)\nTitle: La Vie Parisienne: POPL trip report\n\n Our POPL attendees
will tell us about their favourite talks\, the latest research gossip and
show us their most scenic photos from POPL in Paris.\n
UID:107
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170119T140000
DTEND;TZID=Europe/London:20170119T150000
LOCATION:LT1310
SUMMARY:MSP 101: Automata and games for fixpoint logics
DESCRIPTION:Speaker: Johannes Marti (MSP)\nTitle: MSP 101: Automata and
games for fixpoint logics\n\nI explain how we can use automata and games
to understand the behaviour of modal fixpoint logics.\n
UID:106
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20170112T114000
DTEND;TZID=Europe/London:20170112T124000
LOCATION:LT1310
SUMMARY:Event: MSP101 Planning session
DESCRIPTION:
UID:105
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161214T160000
DTEND;TZID=Europe/London:20161214T170000
LOCATION:LT1415
SUMMARY:Departmental seminar: Do be do be do
DESCRIPTION:Speaker: Sam Lindley (Edinburgh)\nTitle: Do be do be do\n\nWe
explore the design and implementation of Frank\, a strict functional
programming language with a bidirectional effect type system designed
from the ground up around a novel variant of Plotkin and Pretnar's effect
handler abstraction.\n\nEffect handlers provide an abstraction for
modular effectful programming: a handler acts as an interpreter for a
collection of commands whose interfaces are statically tracked by the
type system. However\, Frank eliminates the need for an additional effect
handling construct by generalising the basic mechanism of functional
abstraction itself. A function is simply the special case of a Frank
/operator/ that interprets no commands.\n\nMoreover\, Frank's operators
can be /multihandlers/ which simultaneously interpret commands from
several sources at once\, without disturbing the direct style of
functional programming with values.\n\nEffect typing in Frank employs a
novel form of effect polymorphism which avoid mentioning effect variables
in source code. This is achieved by propagating an /ambient ability/
inwards\, rather than accumulating unions of potential effects
outwards.\n\nI'll give a tour of Frank through a selection of concrete
examples.\n\n(Joint work with Conor McBride and Craig McLaughlin) \n
UID:104
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161130T120000
DTEND;TZID=Europe/London:20161130T130000
LOCATION:Strathclyde
SUMMARY:Event: CLAP
DESCRIPTION:
UID:103
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161102T140000
DTEND;TZID=Europe/London:20161102T150000
LOCATION:LT1415
SUMMARY:An introduction to many-valued logics and effect algebras
DESCRIPTION:Speaker: Phil Scott (University of Ottawa)\nTitle: An
introduction to many-valued logics and effect algebras\n\nThe algebras of
many-valued Lukasiewicz logics (MV algebras) as well as the theory of
quantum measurement (Effect algebras) have undergone considerable
development in the 1980s and 1990s\; they now constitute important
research fields\, with connections to several contemporary areas of
mathematics\, logic\, and theoretical computer science.\n\nBoth subjects
have recently attracted considerable interest among groups of researchers
in categorical logic and foundations of quantum computing. I will give a
leisurely introduction to MV algebras (and their associated logics)\, as
well as the more general world of effect algebras. If time permits\, we
will also illustrate some new results (with Mark Lawson\, Heriot-Watt) on
coordinatization of some concrete MV-algebras using inverse semigroup
theory.\n
UID:102
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161109T120000
DTEND;TZID=Europe/London:20161109T130000
LOCATION:Room 301\, McCance building\, Strathclyde
SUMMARY:Event: SPLS
DESCRIPTION:
UID:101
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160928T150000
DTEND;TZID=Europe/London:20160928T160000
LOCATION:LT1310
SUMMARY:Towards a Generic Treatment of Syntaxes with Binding
DESCRIPTION:Speaker: Guillaume Allais (Radboud University
Nijmegen)\nTitle: Towards a Generic Treatment of Syntaxes with
Binding\n\nThe techniques used by the generic programming community have
taught us that we can greatly benefit from exposing the common internal
structure of a family of objects. One can for instance derive once and
for all a wealth of iterators from an abstract characterisation of
recursive datatypes as fixpoints of functors.\n\nOur previous work on
type and scope preserving semantics and their properties has made us
realise that numerous semantics of the lambda calculus can be presented
as instances of the fundamental lemma associated to an abstract notion of
'Model'. This made it possible to avoid code duplication as well as prove
these semantics' properties generically.\n\nPutting these two ideas
together\, we give an abstract description of syntaxes with binding
making both their recursive and scoping structure explicit. The
fundamental lemma associated to these syntaxes can be instantiated to
provide the user with proofs that its language is stable under renaming
and substitution as well as provide a way to easily define various
evaluators.\n
UID:100
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160915T150000
DTEND;TZID=Europe/London:20160915T160000
LOCATION:LT1310
SUMMARY:Morphisms of open games
DESCRIPTION:Speaker: Jules Hedges (Oxford)\nTitle: Morphisms of open
games\n\n\n
UID:99
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161214T110000
DTEND;TZID=Europe/London:20161214T120000
LOCATION:LT1310
SUMMARY:Compositional Game Theory
DESCRIPTION:Speaker: Alasdair Lambert (MSP)\nTitle: Compositional Game
Theory\n\nI will be discussing composition in a model of economic game
theory and methods for representing the impact of choice on subsequent
games. Time permitting I will also work through some games using this
model.\n
UID:98
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161207T110000
DTEND;TZID=Europe/London:20161207T120000
LOCATION:LT1310
SUMMARY:Nominal filters and semantics of predicate logic
DESCRIPTION:Speaker: Jamie Gabbay (Heriot-Watt)\nTitle: Nominal filters
and semantics of predicate logic\n\nA /filter/ P is a consistent
deductively closed set of predicates. A filter is /prime/ when\n (phi or
psi) in P => (phi in P or psi in P) \nIn words: if phi-or-psi is in P
then phi is in P or psi is in P. Primeness gives soundness for
disjunction.\n\nUsing this it is not hard to construct a semantics to
propositional logic in which a predicate phi "means" the set of prime
filters containing it. This is a standard "trick" for building semantics
and is an extremely useful proof-method.\n\nI have developed a semantics
for predicate logic and also for the lambda-calculus based on similar
notions of filter\, but in a /nominal/ context --- meaning that filters
are developed using Fraenkel-Mostowski (FM) set theory instead of
Zermelo-Fraenkel (ZF) set theory. What matters here is that FM sets have
additional name structure over ZF sets\, and this additional structure
can be exploited to give semantics to the extra structure that predicates
have over propositions\, and in particular the additional name structure
lets us write down primeness conditions for soundness for universal
quantification.\n\nThe resulting semantics is rich and interesting. In a
sentence: nominal techniques help us to extend the notion of Stone
representation and duality from propositional logic to full first-order
logic (also with equality\, if we wish\, and also to other logics and
calculi with variables and quantifiers).\n\nI will give a detailed
description of the filter-style conditions involved\, and discuss some of
what I think they tell us about predicates and quantification in logic
and computation. More information can also be found in two papers
here:\nhttp://www.gabbay.org.uk/papers.html#semooc\nhttp://www.gabbay.org.uk/papers.html#repdul\n
UID:97
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161123T110000
DTEND;TZID=Europe/London:20161123T120000
LOCATION:LT1310
SUMMARY:Some model theory for the modal mu-calculus
DESCRIPTION:Speaker: Yde Venema (ILLC\, Amsterdam)\nTitle: Some model
theory for the modal mu-calculus\n\nWe discuss a number of semantic
properties pertaining to formulas of the modal mu-calculus. For each of
these properties we provide a corresponding syntactic fragment\, in the
sense that a mu-calculus formula \\phi has the given property iff it is
equivalent to a formula \\phi' in the corresponding fragment. Since this
formula \\phi' will always be effectively obtainable from \\phi\, as a
corollary\, for each of the properties under discussion\, we prove that
it is decidable in elementary time whether a given mu-calculus formula
has the property or not.\n\nThe properties that we study have in common
that they all concern the dependency of the truth of the formula at
stake\, on a single proposition letter p. In each case the semantic
condition on \\phi will be that \\phi\, if true at a certain state in a
certain model\, will remain true if we restrict the set of states where p
holds\, to a special subset of the state space. Important examples
include the properties of complete additivity and (Scott) continuity\,
where the special subsets are the singletons and the finite sets\,
respectively.\n\nOur proofs for these characterisation results will be
automata-theoretic in nature\; we will see that the effectively defined
maps on formulas are in fact induced by rather simple transformations on
modal automata.\n
UID:96
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161116T110000
DTEND;TZID=Europe/London:20161116T120000
LOCATION:LT1310
SUMMARY:MSP 101: Modal logic
DESCRIPTION:Speaker: Johannes Marti (MSP)\nTitle: MSP 101: Modal
logic\n\nModal logic provides a simple\, yet surprisingly powerful\,
language for specifying properties of coalgebras. In this talk I
introduce the basic modal logic that is interpreted on relational
structures. My aim is to provide an idea how modal logic relates to other
logics\, such as first-order and intuitionistic logic\, and to the
duality between algebraic and coalgebraic structures.\n\nIf time
permits\, I might also give a very informal warm-up for the modal
mu-calculus which is the topic of next week's talk.\n
UID:95
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161109T103000
DTEND;TZID=Europe/London:20161109T113000
LOCATION:LT1310
SUMMARY:MSP 101: Meta-theory of lambda-calculi
DESCRIPTION:Speaker: Stuart Gale (MSP)\nTitle: MSP 101: Meta-theory of
lambda-calculi\n\nI'll give a standard overview of Simply Typed Lambda
Calculus (STLC) (syntax\, typing and computation rules) in a well-typed
setting\, and then modify it to show STLC in a bidirectional
setting.\n\nAfterwards I'll show Strong Confluence (Church-Rosser
theorem) in the bidirectional setting.\n
UID:94
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161102T110000
DTEND;TZID=Europe/London:20161102T120000
LOCATION:LT1310
SUMMARY:System F and proof-relevant parametricity
DESCRIPTION:Speaker: Ben Price (MSP)\nTitle: System F and proof-relevant
parametricity\n\nI shall give a brief introduction to System F.\nI will
then explain how to capture our intuition about polymorphic functions
behaving uniformly by relational parametricity\, and talk about ongoing
work to find a notion of proof-relevant parametricity.\n
UID:93
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161026T110000
DTEND;TZID=Europe/London:20161026T120000
LOCATION:LT1310
SUMMARY:MSP 101: Data types and initial-algebra semantics
DESCRIPTION:Speaker: Fredrik Nordvall Forsberg (MSP)\nTitle: MSP 101:
Data types and initial-algebra semantics\n\nI will give a basic
introduction to data types and initial-algebra semantics. The meaning of
a data type is given as the initial object in a category of types with
the corresponding constructors. Initiality immediately allows the
modelling of a non-dependent recursion principle. I'll show how this can
be upgraded to full dependent elimination\, also known as induction\, by
using the uniqueness of the mediating arrow\; in fact\, induction is
equivalent to recursion plus uniqueness. All possibly unfamiliar terms in
this abstract will also be explained.\n
UID:92
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161019T110000
DTEND;TZID=Europe/London:20161019T120000
LOCATION:LT1310
SUMMARY:MSP 101: A first introduction to coalgebra
DESCRIPTION:Speaker: Clemens Kupke (MSP)\nTitle: MSP 101: A first
introduction to coalgebra\n\nThe core subject of Computer Science is
"generated behaviour" (quiz: who said this?). Coalgebra provides the
categorical formalisation of generated behaviour. I am planning to
provide a first\, very basic introduction to coalgebra. This will consist
of two parts: i) coinduction & corecursion as means to define & reason
about the (possibly) infinite behaviour of things\; ii)modal logics for
coalgebras.\n
UID:91
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161012T110000
DTEND;TZID=Europe/London:20161012T120000
LOCATION:LT1310
SUMMARY:MSP 101: Category Theory
DESCRIPTION:Speaker: Neil Ghani (MSP)\nTitle: MSP 101: Category
Theory\n\n\n
UID:90
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20161005T110000
DTEND;TZID=Europe/London:20161005T120000
LOCATION:LT1310
SUMMARY:MSP 101: Rewriting\, and operads
DESCRIPTION:Speaker: Ross Duncan (MSP)\nTitle: MSP 101: Rewriting\, and
operads\n\n\n
UID:89
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160928T110000
DTEND;TZID=Europe/London:20160928T120000
LOCATION:LT1310
SUMMARY:ICFP trip report
DESCRIPTION:Speaker: James Chapman (MSP)\nTitle: ICFP trip report\n\n\n
UID:88
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160921T110000
DTEND;TZID=Europe/London:20160921T120000
LOCATION:LT1310
SUMMARY:Eventual image functors
DESCRIPTION:Speaker: Kevin Dunne (MSP)\nTitle: Eventual image
functors\n\nFor a category C we consider the endomorphism category End(C)
and the subcategory of automorphisms Aut(C) -> End(C). It has been
observed that for C the category of finite sets\, finite dimensional
vector spaces\, or compact metric spaces this inclusion functor admits a
simultaneous left and right adjoint.\n\nWe give general criteria for the
existence of such adjunctions for a broad class of categories which
includes FinSet\, FinVect and CompMet as special cases. This is done
using the language of factorisation systems and by introducing a notion
of eventual image functors which provide a general method for
constructing adjunctions of this kind.\n
UID:87
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160914T114000
DTEND;TZID=Europe/London:20160914T124000
LOCATION:LT1310
SUMMARY:Event: MSP101 Planning session
DESCRIPTION:
UID:86
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160824T160000
DTEND;TZID=Europe/London:20160824T170000
LOCATION:LT1415
SUMMARY:Information Effects for Understanding Type Systems
DESCRIPTION:Speaker: Philippa Cowderoy \nTitle: Information Effects for
Understanding Type Systems\n\nOr: how someone else found the maths to
justify my dogma\n
UID:85
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160701T140000
DTEND;TZID=Europe/London:20160701T150000
LOCATION:LT1415
SUMMARY:A New Perspective On Observables in the Category of Relations
DESCRIPTION:Speaker: Kevin Dunne (MSP)\nTitle: A New Perspective On
Observables in the Category of Relations\n\nPractice talk for Quantum
Interactions.\n
UID:84
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160701T140000
DTEND;TZID=Europe/London:20160701T150000
LOCATION:LT1415
SUMMARY:Interacting Frobenius Algebras are Hopf
DESCRIPTION:Speaker: Ross Duncan (MSP)\nTitle: Interacting Frobenius
Algebras are Hopf\n\nPractice talk for LICS.\n\nTheories featuring the
interaction between a Frobenius algebra and a Hopf algebra have recently
appeared in several areas in computer science: concurrent programming\,
control theory\, and quantum computing\, among others. Bonchi\,
Sobocinski\, and Zanasi have shown that\, given a suitable distribution
law\, a pair of Hopf algebras forms two Frobenius algebras. Coming from
the perspective of quantum theory\, we take the opposite approach\, and
show that interacting Frobenius algebras form Hopf algebras. We
generalise \\cite{Bonchi2014a} by including non-trivial dynamics of the
underlying object -- the so-called phase group -- and investigate the
effects of finite dimensionality of the underlying model\, and recover
the system of Bonchi et al as a subtheory in the prime power dimensional
case. We show that the presence of a non-trivial phase group means that
the theory cannot be formalised as a distributive law.\n
UID:83
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160606T090000
DTEND;TZID=Europe/London:20160606T100000
LOCATION:McCance building\, Strathclyde
SUMMARY:Event: Quantum Physics and Logic 2016
DESCRIPTION:
UID:82
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160601T120000
DTEND;TZID=Europe/London:20160601T130000
LOCATION:LT1310
SUMMARY:Interacting Frobenius algebras
DESCRIPTION:Speaker: Kevin Dunne (MSP)\nTitle: Interacting Frobenius
algebras\n\nPractice talk for QPL.\n\nTheories featuring the interaction
between a Frobenius algebra and a Hopf algebra have recently appeared in
several areas in computer science: concurrent programming\, control
theory\, and quantum computing\, among others. Bonchi\, Sobocinski\, and
Zanasi (2014) have shown that\, given a suitable distributive law\, a
pair of Hopf algebras forms two Frobenius algebras. Here we take the
opposite approach\, and show that interacting Frobenius algebras form
Hopf algebras. We generalise (BSZ 2014) by including non-trivial dynamics
of the underlying object---the so-called phase group---and investigate
the effects of finite dimensionality of the underlying model. We recover
the system of Bonchi et al as a subtheory in the prime power dimensional
case\, but the more general theory does not arise from a distributive
law.\n
UID:81
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160504T110000
DTEND;TZID=Europe/London:20160504T120000
LOCATION:LT1310
SUMMARY:Factorisation Systems and Algebra
DESCRIPTION:Speaker: Kevin Dunne (MSP)\nTitle: Factorisation Systems and
Algebra\n\nI'll show how to generalise some results from algebra (think
groups\, rings\, R-modules etc.) to a categorical setting using
factorisation systems and an appropriate notion of finiteness on the
objects of a category.\n
UID:80
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160427T110000
DTEND;TZID=Europe/London:20160427T120000
LOCATION:LT1310
SUMMARY:Typing with Leftovers
DESCRIPTION:Speaker: Guillaume Allais (Radboud University
Nijmegen)\nTitle: Typing with Leftovers\n\n\n
UID:79
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160419T160000
DTEND;TZID=Europe/London:20160419T170000
LOCATION:LT1415
SUMMARY:Departmental seminar: Formal languages\, coinductively formalized
DESCRIPTION:Speaker: Andreas Abel (Chalmers and Gothenburg
University)\nTitle: Formal languages\, coinductively formalized\n\nFormal
languages and automata are taught to every computer science student.
However\, the student will most likely not see the beautiful coalgebraic
foundations.\n\nIn this talk\, I recapitulate how infinite trees can
represent formal languages (sets of strings). I explain Agda's
coinduction mechanism based on copatterns and demonstrate that it allows
an elegant representation of the usual language constructions like
union\, concatenation\, and Kleene star\, with the help of Brzozowski
derivatives. We will also investigate how to reason about equality of
languages using bisimulation and coinductive proofs.\n
UID:78
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160414T103000
DTEND;TZID=Europe/London:20160414T113000
LOCATION: School of Informatics\, Edinburgh
SUMMARY:Event: Categories\, Logic\, and Physics\, Scotland
DESCRIPTION:
UID:77
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160331T103000
DTEND;TZID=Europe/London:20160331T113000
LOCATION:LT1415
SUMMARY:Presentations by candidates for the 'Coalgebraic Foundations of
Semi-Structured Data' RA position
DESCRIPTION:Speaker: \nTitle: Presentations by candidates for the
'Coalgebraic Foundations of Semi-Structured Data' RA position\n\n\n
UID:76
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160323T160000
DTEND;TZID=Europe/London:20160323T170000
LOCATION:LT1415
SUMMARY:Departmental seminar: A static analyser for concurrent Java
DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: A static analyser for
concurrent Java\n\nThreadSafe is a static analysis tool for finding bugs
in concurrent Java code that has been used by companies across the world
to analyse and find bugs in large mission industrial applications. I will
talk about how ThreadSafe works\, and our experiences in applying static
analysis technology to the "real world".\n\nThreadSafe is available from
http://www.contemplateltd.com/\n
UID:75
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160525T153000
DTEND;TZID=Europe/London:20160525T163000
LOCATION:LT908
SUMMARY:Departmental seminar: A Compositional Approach to Game Theory
DESCRIPTION:Speaker: Neil Ghani (MSP)\nTitle: A Compositional Approach to
Game Theory\n\nI will sketch an alternative approach to economic game
theory based upon the computer science idea of compositionality:
concretely we i) give a number of operators for building up complex and
irregular games from smaller and simpler games\; and ii) show how the
Nash equilibrium of these complex games can be defined recursively from
their simpler components. We apply compositional reasoning to
sophisticated games where agents must reason about how their actions
affect future games and how those future games effect the utility they
receive. This forces us into a second innovation -- we augment the usual
lexicon of games with a dual notion to utility because\, in order for
games to accept utility\, this utility must be generated by other games.
Our third innovation is to represent our games as string diagrams so as
to give a clear visual interface to manipulate them. Our fourth\, and
final\, innovation is a categorical formalisation of these intuitive
diagrams which ensures our reasoning about them is fully rigorous.\n\nThe
talk will be general so as appeal to as wide an audience as possible. In
particular\, no knowledge of category theory will be assumed!\n
UID:74
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160317T110000
DTEND;TZID=Europe/London:20160317T120000
LOCATION:LT1310
SUMMARY:On the rule algebraic reformulation of graph rewriting
DESCRIPTION:Speaker: Nicolas Behr (Edinburgh)\nTitle: On the rule
algebraic reformulation of graph rewriting\n\nMotivated by the desire to
understand the combinatorics of graph rewriting systems\, it proved
necessary to invent a formulation of graph rewriting itself that is not
based on category theoretic structures as in the traditional framework\,
but on the concept of diagrammatic combinatorial Hopf algebras and
reductions thereof. In this talk\, I will present how the classical
example of the Heisenberg-Weyl algebra of creation and annihilation of
indistinguishable particles\, which can alternatively be interpreted as
the algebra of discrete graph rewriting\, gave the initial clues for this
novel framework. In hindsight\, to pass from the special case of discrete
graph rewriting to the case of general graph rewriting required every
aspect of the framework of diagrammatic combinatorial Hopf algebras as a
guideline for the construction\, yet none of the traditional category
theoretic ideas\, whence one might indeed consider this reformulation as
an independent formulation of graph rewriting.\n\nThe new framework
results in a number of surprising results even directly from the
formulation itself: besides the two main variants of graph rewriting
known in the literature (DPO and SPO rewriting)\, there exist two more
natural variants in the new framework. For all four variants\, graph
rewriting rules are encoded in so-called rule diagrams\, with their
composition captured in the form of diagrammatic compositions followed by
one of four variants of reduction operations. Besides the general
structure theory of the resulting algebras aka the rule algebras\, one of
the most important results to date of this framework in view of
applications is the possibility to formulate stochastic graph rewriting
systems in terms of the canonical representations of the rule algebras.
Notably\, this is closely analogous to the formulation of chemical
reaction systems in terms of the canonical representation of the
Heisenberg-Weyl algebra aka the bosonic Fock space. The presentation will
not assume any prior knowledge of the audience on the particular
mathematics required for this construction\, and will be given on the
whiteboard. The work presented is the result of a collaboration with
Vincent Danos and Ilias Garnier (ENS Paris/LFCS University of
Edinburgh)\, and (in an earlier phase) with Tobias Heindel (University of
Copenhagen).\n
UID:73
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160303T110000
DTEND;TZID=Europe/London:20160303T120000
LOCATION:LT1310
SUMMARY:Comprehensive Parametric Polymorphism
DESCRIPTION:Speaker: Fredrik Nordvall Forsberg (MSP)\nTitle:
Comprehensive Parametric Polymorphism\n\nIn this talk\, we explore the
fundamental category-theoretic structure needed to model relational
parametricity (i.e.\, the fact that polymorphic programs preserve all
relations) for the polymorphic lambda calculus (a.k.a. System F). Taken
separately\, the notions of categorical model of impredicative
polymorphism and relational parametricity are well-known
(lambda2-fibrations and reflexive graph categories\, respectively).
Perhaps surprisingly\, simply combining these two structures results in a
notion that only enjoys the expected properties in case the underlying
category is well-pointed. This rules out many categories of interest
(e.g. functor categories) in the semantics of programming
languages.\n\nTo circumvent this restriction\, we modify the definition
of fibrational model of impredicative polymorphism by adding one further
ingredient to the structure: comprehension in the sense of Lawvere. Our
main result is that such comprehensive models\, once further endowed with
reflexive-graph-category structure\, enjoy the expected consequences of
parametricity. This is proved using a type-theoretic presentation of the
category-theoretic structure\, within which the desired consequences of
parametricity are derived. Working in this type theory requires new
techniques\, since equality relations are not available\, so that
standard arguments that exploit equality need to be reworked.\n\nThis is
joint work with Neil Ghani and Alex Simpson\, and a dry run for a talk in
Cambridge the week after.\n
UID:72
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160126T150000
DTEND;TZID=Europe/London:20160126T160000
LOCATION:LT1310
SUMMARY:Rewriting modulo symmetric monoidal structure
DESCRIPTION:Speaker: Aleks Kissinger (Nijmegen)\nTitle: Rewriting modulo
symmetric monoidal structure\n\nString diagrams give a powerful graphical
syntax for morphisms in symmetric monoidal categories (SMCs). They find
many applications in computer science and are becoming increasingly
relevant in other fields such as physics and control theory.\n\nAn
important role in many such approaches is played by equational theories
of diagrams\, which can be oriented and used as rewrite systems. In this
talk\, I'll lay the foundations for this form of rewriting by
interpreting diagrams combinatorially as typed hypergraphs and establish
the precise correspondence between diagram rewriting modulo the laws of
SMCs on the one hand and double pushout (DPO) rewriting of hypergraphs\,
subject to a soundness condition called convexity\, on the other. This
result rests on a more general characterisation theorem in which we show
that typed hypergraph DPO rewriting amounts to diagram rewriting modulo
the laws of SMCs with a chosen special Frobenius structure.\n\nIf there's
time\, I'll also discuss some of the results we have in developing the
rewrite theory of hypergraphs for SMCs\, namely termination proofs via
graph metrics and strongly convex critical pair analysis.\n
UID:71
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160126T103000
DTEND;TZID=Europe/London:20160126T113000
LOCATION:LT1310
SUMMARY:Enriched Lawvere Theories
DESCRIPTION:Speaker: John Power (Bath)\nTitle: Enriched Lawvere
Theories\n\nIn this talk\, we consider extending Lawvere theories to
allow enrichment in a base category such as CMonoid\, Poset or Cat. In
doing so\, we see that we need to alter the formulation in a fundamental
way\, using the notion of cotensor\, a kind of limit that is hidden in
the usual accounts of ordinary category theory but is fundamental to
enriched category theory. If time permits\, we will briefly consider the
specific issues that arise when one has two-dimensional structure in the
enriching category\, as exemplified by Poset and Cat.\n
UID:70
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160125T103000
DTEND;TZID=Europe/London:20160125T113000
LOCATION:LT1310
SUMMARY:Lawvere Theories
DESCRIPTION:Speaker: John Power (Bath)\nTitle: Lawvere Theories\n\nIn
1963\, Bill Lawvere characterised universal algebra in category theoretic
terms. His formulation being category theoretic was not its central
contribution: more fundamental was its presentation independence. Three
years later\, monads were proposed as another category theoretic
formulation of universal algebra. Overall\, the former are technically
better but the relationship is particularly fruitful and the latter are
more prominent\, cf Betamax vs VHS. So we study Lawvere theories
carefully in the setting of universal algebra and in relation to
monads.\n
UID:69
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160225T110000
DTEND;TZID=Europe/London:20160225T120000
LOCATION:LT1310
SUMMARY:Excuse My Extrusion
DESCRIPTION:Speaker: Conor McBride (MSP)\nTitle: Excuse My Extrusion\n\nI
have recently begun to learn about the Cubical Type Theory of Coquand et
al.\, as an effective computational basis for Voevodsky's Univalent
Foundations\, inspired by a model of type theory in cubical sets. It is
in some ways compelling in its simplicity\, but in other ways
intimidating in its complexity. In order to get to grips with it\, I have
begun to develop my own much less subtle variation on the theme. If I am
lucky\, I shall get away with it. If I am unlucky\, I shall have learned
more about why Cubical Type Theory has to be as subtle as it is.\n\nMy
design separates Coquand's all-powerful "compose" operator into smaller
pieces\, dedicated to more specific tasks\, such as transitivity of
paths. Each type path Q : S = T\, induces a notion of value path s {Q}
t\, where either s : S\, or s is •\, "blob"\, and similarly\, t : T or t
= •. A "blob" at one end indicates that the value at that end of the path
is not mandated by the type. This liberalisation in the formation of
"equality" types allows us to specify the key computational use of paths
between types\, extrusion:\n\nif Q : S = T and s : S\, then s ⌢• Q : s
{Q} •\n\nThat is\, whenever we have a value s at one end of a type path Q
: S = T\, we can extrude that value across the type path\, getting a
value path which is s at the S end\, but whose value at the T end is not
specified in advance of explaining how to compute it. Extrusion gives us
a notion of coercion-by-equality which is coherent by construction. It is
defined by recursion on the structure of type paths. Univalence can be
added to the system by allowing the formation of types interpolating two
equivalent types\, with extrusion demanding the existence of the
corresponding interpolant values\, computed on demand by means of the
equivalence.\n\nSo far\, there are disconcerting grounds for optimism\,
but the whole of the picture has not yet emerged: I may just have pushed
the essential complexity into one corner\, or the whole thing may be
holed below the waterline. But if it does turn out to be nonsense\, it
will be nonsense for an interesting reason.\n
UID:68
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160218T140000
DTEND;TZID=Europe/London:20160218T150000
LOCATION:LT1310
SUMMARY:Coalgebraic Dynamic Logics
DESCRIPTION:Speaker: Clemens Kupke (MSP)\nTitle: Coalgebraic Dynamic
Logics\n\nI will present work in progress on a (co)algebraic framework
that allows to uniformly study dynamic modal logics such as Propositional
Dynamic Logic (PDL) and Game Logic (GL). Underlying our framework is the
basic observation that the program/game constructs of PDL/GL arise from
monad structure\, and that the axioms of these logics correspond to
compatibility requirements between the modalities and this monad
structure. So far we have a general soundness and completeness result for
PDL-like logics wrt T-coalgebras for a monad T. I will discuss our
completeness theorem\, its limitations and plans for extending our
results. [For the latter we might require the help of koalas\, wallabies
and wombats.]\n
UID:67
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160211T110000
DTEND;TZID=Europe/London:20160211T120000
LOCATION:LT1310
SUMMARY:Introduction to (infinity\, 1)-categories
DESCRIPTION:Speaker: Fredrik Nordvall Forsberg (MSP)\nTitle: Introduction
to (infinity\, 1)-categories\n\nInfinity-categories simultaneously
generalise topological spaces and categories. Intuitively\, a (weak)
infinity-category should have objects\, morphisms\, 2-morphisms\,
3-morphisms\, ... and identity morphisms and composition which is
suitably unital and associative up to a higher (invertible) morphism (the
number 1 in (infinity\, 1)-category means that k-morphisms for k > 1 are
invertible) . The trouble begins when one naively tries to make these
coherence conditions precise\; already 4-categories famously requires 51
pages to define explicitly
(http://math.ucr.edu/home/baez/trimble/tetracategories.html). Instead\,
one typically turns to certain "models" of infinity-categories that
encode all this data implicitly\, usually as some kind of simplicial
object with additional properties. I will introduce two such models:
quasicategories and complete Segal spaces. If time allows\, I will also
discuss hopes and dreams about internalising these notions in Type
Theory\, which should give a satisfactory treatment of category theory in
Type Theory without assuming Uniqueness of Identity Proofs.\n
UID:66
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160204T110000
DTEND;TZID=Europe/London:20160204T120000
LOCATION:LT1310
SUMMARY:Two Constructions on Games
DESCRIPTION:Speaker: Neil Ghani (MSP)\nTitle: Two Constructions on
Games\n\nI've been working with Jules Hedges on a compositional model of
game theory. After briefly reminding you of the model\, I'll discuss
where we are at -- namely the definition of morphisms between games\, and
the treatment of choice and iteration of games. I'm hoping you will be
able to shed some light on this murky area. There is a draft paper if
anyone is interested.\n
UID:65
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160128T110000
DTEND;TZID=Europe/London:20160128T120000
LOCATION:LT1310
SUMMARY:Introduction to sheaves
DESCRIPTION:Speaker: Kevin Dunne (MSP)\nTitle: Introduction to
sheaves\n\n\n
UID:64
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160121T110000
DTEND;TZID=Europe/London:20160121T120000
LOCATION:LT1310
SUMMARY:Overview: A Type Theory for Probabilistic and Bayesian Reasoning
DESCRIPTION:Speaker: Guillaume Allais (MSP)\nTitle: Overview: A Type
Theory for Probabilistic and Bayesian Reasoning\n\nThe probabilistic
calculus introduced in the eponymous paper by Robin Adams and Bart Jacobs
is inspired by quantum theory by considering that conditional
probabilities can be seen as side-effect-free measurements. A
type-theoretic treatment of this semantic observation leads\, once
equipped with suitable computation rules\, to the ability to do exact
conditional inference.\n\nI will present the type theory and the
accompanying computation rules proposed in the paper and discuss some of
the interesting open questions I will be working on in the near future.
\n
UID:63
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20160113T134000
DTEND;TZID=Europe/London:20160113T144000
LOCATION:LT1310
SUMMARY:Event: MSP101 Planning session
DESCRIPTION:
UID:62
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20151202T110000
DTEND;TZID=Europe/London:20151202T120000
LOCATION:LT1310
SUMMARY:Introduction to coherence spaces\, and how to use them for
dependent session types
DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: Introduction to coherence
spaces\, and how to use them for dependent session types\n\nCoherence
spaces are a simplification of Scott domains\, introduced by Girard to
give a semantics to the polymorphic lambda-calculus. While investigating
the structure of coherence spaces\, Girard noticed that the denotation of
the function type in coherence spaces can be decomposed into two
independent constructions: a linear ("use-once") function space\, and a
many-uses-into-one-use modality. And so Linear Logic was
discovered.\n\nCoherence spaces are interesting because they model
computation at a low level in terms of interchange of atomic 'tokens' of
information. This makes them a useful tool for understanding several
different computational phenomena.\n\nIn this talk\, I'll show how
coherence spaces naturally model session types\, via Wadler's
interpretation of Classical Linear Logic as a session-typed pi-calculus\,
and how that interpretation extends to an interpretation of a dependently
typed version of session types.\n
UID:61
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20151118T110000
DTEND;TZID=Europe/London:20151118T120000
LOCATION:LT1310
SUMMARY:The categorical structure of von Neumann algebras
DESCRIPTION:Speaker: Bram Westerbaan (Nijmegen)\nTitle: The categorical
structure of von Neumann algebras\n\nI would like to speak about the
categorical structure of the category of von Neumann algebras\, with as
morphisms normal\, completely positive\, unital linear maps. For some
years my colleagues and I have worked on identifying basic structures in
this category\, and while surprisingly many things do not exist or do not
work in this category (it's not a topos or even an extensive category\,
there's no epi-mono factorisation system\, there is no dagger\, colimits
-- if they exist at all -- are horrendous...)\, we did find some
structure (the products behave reasonable in some sense\, there is a
'quotient'\, and 'comprehension'\, and we have a universal property for
the minimal Stinespring dilation\, and a universal property for M_2--the
qubit). There is no deep category theory involved by any standards\, and
I promise I will spare you the functional analysis\, so it should be a
light talk.\n
UID:60
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20151111T110000
DTEND;TZID=Europe/London:20151111T120000
LOCATION:LT1310
SUMMARY:The Power of Coalitions
DESCRIPTION:Speaker: Clemens Kupke (MSP)\nTitle: The Power of
Coalitions\n\nDue to popular demand I am going to give a brief
introduction to Marc Pauly's Coalition Logic\, a propositional modal
logic that allows to reason about the power of coalitions in strategic
games. I will provide motivation and basic definitions. Furthermore I am
planning to discuss how the logic can be naturally viewed as a
coalgebraic logic and what we gain from the coalgebraic perspective.
Finally -- if (preparation) time permits -- I am going to say how the
logic can be applied to the area of mechanism design.\n
UID:59
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20151022T150000
DTEND;TZID=Europe/London:20151022T160000
LOCATION:LT1415
SUMMARY:Semantics for Social Systems where Theory about the System
Changes the System
DESCRIPTION:Speaker: Viktor Winschel (ETH Zurich)\nTitle: Semantics for
Social Systems where Theory about the System Changes the System\n\nIn
societies the notion of a law is not given by nature. Instead social
dynamics are driven by the theories the citizens have about the dynamics
of the social system. Obviously self-referential mathematical
structures\, developed in computer science\, are candidates to be applied
in social sciences for this foundational issue. We will see a
prototypical game theoretical problem where several computer scientific
tools can help to discuss these structures. It is a long standing problem
in economics and of human kind and their scarce recourses: "should we go
to a bar that is always so overcrowded"?\n
UID:58
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20151006T150000
DTEND;TZID=Europe/London:20151006T160000
LOCATION:LT1415
SUMMARY:Proof-theoretic semantics for dynamic logics
DESCRIPTION:Speaker: Alessandra Palmigiano (TU Delft)\nTitle:
Proof-theoretic semantics for dynamic logics\n\nResearch in the proof
theory of dynamic logics has recently gained momentum. However\, features
which are essential to these logics prevent standard proof-theoretic
methodologies to apply straightforwardly. In this talk\, I will discuss
the main properties proof systems should enjoy in order to serve as
suitable environments for an inferential theory of meaning
(proof-theoretic semantics). Then\, I'll identify the main challenges to
the inferential semantics research agenda posed by the very features of
dynamic logics which make them so appealing and useful to applications.
Finally\, I'll illustrate a methodology generating multi-type display
calculi\, which has been successful on interesting case studies (dynamic
epistemic logic\, propositional dynamic logic\, monotone modal
logic).\n\nReferences\n\n1. S. Frittella\, G. Greco\, A. Kurz\, A.
Palmigiano\, V. Sikimić\, A Proof-Theoretic Semantic Analysis of Dynamic
Epistemic Logic\, Journal of Logic and Computation\, Special issue on
Substructural logic and information dynamics (2014)\,
DOI:10.1093/logcom/exu063.\n\n2. S. Frittella\, G. Greco\, A. Kurz\, A.
Palmigiano\, V. Sikimić\, Multi-type Display Calculus for Dynamic
Epistemic Logic\, Journal of Logic and Computation\, Special issue on
Substructural logic and information dynamics (2014)\,
DOI:10.1093/logcom/exu068.\n\n3. S. Frittella\, G. Greco\, A. Kurz\, A.
Palmigiano\, Multi-type Display Calculus for Propositional Dynamic
Logic\, Special issue on Substructural logic and information dynamics
(2014)\, DOI:10.1093/logcom/exu064.\n\n4. S. Frittella\, G. Greco\, A.
Kurz\, A. Palmigiano\, V. Sikimić\, Multi-type Sequent Calculi\, Proc.
Trends in Logic XIII\, A. Indrzejczak\, J. Kaczmarek\, M. Zawidski eds\,
p 81-93\, 2014.\n\n5. G. Greco\, A. Kurz\, A. Palmigiano\, Dynamic
Epistemic Logic Displayed\, Proc. Fourth International Workshop on
Logic\, Rationality and Interaction (LORI 2013) Eds: Huaxin Huang\,
Davide Grossi\, Olivier Roy eds\, 2013.\n
UID:57
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150925T160000
DTEND;TZID=Europe/London:20150925T170000
LOCATION:LT1415
SUMMARY:Coinduction\, Equilibrium and Rationality of Escalation
DESCRIPTION:Speaker: Pierre Lescanne (ENS Lyon)\nTitle: Coinduction\,
Equilibrium and Rationality of Escalation\n\nEscalation is the behavior
of players who play forever in the same game. Such a situation is a
typical field for application of coinduction which is the tool conceived
for reasoning in infinite mathematical structures. In particular\, we use
coinduction to study formally the game called --dollar auction--\, which
is considered as the paradigm of escalation. Unlike what is admitted
since 1971\, we show that\, provided one assumes that the other agent
will always stop\, bidding is rational\, because it results in a subgame
perfect equilibrium. We show that this is not the only rational strategy
profile (the only subgame perfect equilibrium). Indeed if an agent stops
and will stop at every step\, whereas the other agent keeps bidding\, we
claim that he is rational as well because this corresponds to another
subgame perfect equilibrium. In the infinite dollar auction game the
behavior in which both agents stop at each step is not a Nash
equilibrium\, hence is not a subgame perfect equilibrium\, hence is not
rational. Fortunately\, the notion of rationality based on coinduction
fits with common sense and experience. Finally the possibility of a
rational escalation in an arbitrary game can be expressed as a predicate
on games and the rationality of escalation in the dollar auction game can
be proved as a theorem which we have verified in the proof assistant COQ.
In this talk we will recall the principles of infinite extensive games
and use them to introduce coinduction and equilibria (Nash equilibrium\,
subgame perfect equilibrium). We will show how one can prove that the two
strategy profiles presented above are equilibria and how this leads to a
"rational" escalation in the dollar auction. We will show that escalation
may even happen in much simpler game named 0,1-game.\n
UID:56
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20151028T110000
DTEND;TZID=Europe/London:20151028T120000
LOCATION:LT1310
SUMMARY:Interacting Frobenius Algebras Are Hopf
DESCRIPTION:Speaker: Ross Duncan (MSP)\nTitle: Interacting Frobenius
Algebras Are Hopf\n\nCommutative Frobenius algebras play an important
role in both Topological Quantum Field Theory and Categorical Quantum
Mechanics\; in the first case they correspond to 2D TQFTs\, while in the
second they are non-degenerate observables. I will consider the case of
"special" Frobenius algebras\, and their associated group of phases. This
gives rise to a free construction from the category of abelian groups to
the PROP generated by this Frobenius algebra. Of course a theory with
only one observable is not very interesting. I will consider how two such
PROPs should be combined\, and show that if the two algebras (i) jointly
form a bialgebra and (ii) their units are "mutually real"\; then they
jointly form a Hopf algebra. This gives a "free" model of a pair of
strongly complementary observables. I will also consider which unitary
maps must exist in such models.\n\nSlides are here
(http://personal.strath.ac.uk/ross.duncan/talks/2015/vienna.pdf) if you
want a preview.\n
UID:55
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20151021T123000
DTEND;TZID=Europe/London:20151021T133000
LOCATION:Edinburgh
SUMMARY:Event: SPLS
DESCRIPTION:
UID:54
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20151014T110000
DTEND;TZID=Europe/London:20151014T120000
LOCATION:LT1310
SUMMARY:Type and Scope Preserving Semantics
DESCRIPTION:Speaker: Guillaume Allais (MSP)\nTitle: Type and Scope
Preserving Semantics\n\nWe introduce a notion of type and scope
preserving semantics generalising Goguen and McKinna's "Candidates for
Substitution" approach to defining one traversal generic enough to be
instantiated to renaming first and then substitution. Its careful
distinction of environment and model values as well as its variation on a
structure typical of a Kripke semantics make it capable of expressing
renaming and substitution but also various forms of Normalisation by
Evaluation as well as\, perhaps more surprisingly\, monadic computations
such as a printing function.\n\nWe then demonstrate that expressing these
algorithms in a common framework yields immediate benefits: we can deploy
some logical relations generically over these instances and obtain for
instance the fusion lemmas for renaming\, substitution and normalisation
by evaluation as simple corollaries of the appropriate fundamental lemma.
All of this work has been formalised in Agda.\n
UID:53
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20151007T120000
DTEND;TZID=Europe/London:20151007T130000
LOCATION:Dundee
SUMMARY:Event: STP
DESCRIPTION:
UID:52
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150930T110000
DTEND;TZID=Europe/London:20150930T120000
LOCATION:LT1310
SUMMARY:ICFP trip report
DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: ICFP trip report\n\n\n
UID:51
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150923T113000
DTEND;TZID=Europe/London:20150923T123000
LOCATION:LT1310
SUMMARY:Event: MSP101 Planning session
DESCRIPTION:
UID:50
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150916T110000
DTEND;TZID=Europe/London:20150916T120000
LOCATION:LT1310
SUMMARY:Contextuality\, path logic and a modal logic for Social Choice
Theory
DESCRIPTION:Speaker: Giovanni Ciná (Amsterdam)\nTitle: Contextuality\,
path logic and a modal logic for Social Choice Theory\n\nSocial Choice
functions are procedures used to aggregate the preferences of individuals
into a collective decision. We outline two recent abstract approaches to
SCFs: a recent sheaf treatment of Arrow's Theorem by Abramsky and a modal
logic studied by Ulle Endriss and myself. We show how to relate the
categorical modelling of Social Choice problems to said work in Modal
Logic. This insight prompts a number of research questions\, from the
relevance of sheaf-like condition to the modelling of properties of SCFs
on varying electorates.\n
UID:49
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150902T110000
DTEND;TZID=Europe/London:20150902T120000
LOCATION:LT1310
SUMMARY:Concurrent games
DESCRIPTION:Speaker: Ross Duncan (MSP)\nTitle: Concurrent games\n\n\n
UID:48
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150813T150000
DTEND;TZID=Europe/London:20150813T160000
LOCATION:LT1415
SUMMARY:The Polymorphic Blame Calculus and Parametricity
DESCRIPTION:Speaker: Jeremy Siek (Indiana University)\nTitle: The
Polymorphic Blame Calculus and Parametricity\n\nThe Polymorphic Blame
Calculus (PBC) of Ahmed et al. (2011) combines polymorphism\, as in
System F\, with type dynamic and runtime casts\, as in the Blame
Calculus. The PBC is carefully designed to ensure relational
parametricity\, that is\, to ensure that type abstractions do not reveal
their abstracted types. The operational semantics of PBC uses runtime
sealing and syntactic barriers to enforce parametricity. However\, it is
an open question as to whether these mechanisms actually guarantee
parametricity for the PBC. Furthermore\, there is some question regarding
what parametricity means in the context of the PBC\, as we have examples
that are morally parametric but not technically so. This talk will review
the design of the PBC with respect to ensuring parametricity and
hopefully start a discussion regarding what parametricity should mean for
the PBC.\n
UID:47
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150826T110000
DTEND;TZID=Europe/London:20150826T120000
LOCATION:LT1310
SUMMARY:Comonadic Cellular Automata II
DESCRIPTION:Speaker: Kevin Dunne (MSP)\nTitle: Comonadic Cellular
Automata II\n\nThis is a sequel to my last 101 where I spoke about
describing cellular automata as algebras of a comonad on Set. I'll
describe how we can make sense of "generalised cellular automata"
(probabilistic/non-deterministic/quantum\, for example) as comonads on
other categories via distributive laws of monads and comonads.\n
UID:46
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150723T110000
DTEND;TZID=Europe/London:20150723T120000
LOCATION:LT1310
SUMMARY:Free interacting observables
DESCRIPTION:Speaker: Ross Duncan (MSP)\nTitle: Free interacting
observables\n\n\n
UID:45
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150526T160000
DTEND;TZID=Europe/London:20150526T170000
LOCATION:LT1415
SUMMARY:Final coalgebras from corecursive algebras
DESCRIPTION:Speaker: Paul Levy (Birmingham)\nTitle: Final coalgebras from
corecursive algebras\n\nWe give a technique to construct a final
coalgebra out of modal logic. An element of the final coalgebra is a set
of modal formulas. The technique works for both the finite and the
countable powerset functors. Starting with a corecursive algebra\, we
coinductively obtain a suitable subalgebra. We see - first with an
example\, and then in the general setting of modal logic on a dual
adjunction - that modal theories form a corecursive algebra\, so that
this construction may be applied.\n\nWe generalize the framework to
categories other than Set\, and look at examples in Poset and in the
opposite category of Set.\n
UID:44
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150513T110000
DTEND;TZID=Europe/London:20150513T120000
LOCATION:LT1310
SUMMARY:Two-dimensional proof-relevant parametricity
DESCRIPTION:Speaker: Federico Orsanigo (MSP)\nTitle: Two-dimensional
proof-relevant parametricity\n\nRelational parametricity is a fundamental
concept within theoretical computer science and the foundations of
programming languages\, introduced by John Reynolds. His fundamental
insight was that types can be interpreted not just as functors on the
category of sets\, but also as equality preserving functors on the
category of relations. This gives rise to a model where polymorphic
functions are uniform in a suitable sense\; this can be used to establish
e.g. representation independence\, equivalences between programs\, or
deriving useful theorems about programs from their type alone.\n\n The
relations Reynolds considered were proof-irrelevant\, which from a type
theoretic perspective is a little limited. As a result\, one might like
to extend his work to deal with proof-relevant\, i.e. set-valued
relations. However naive attempts to do this fail: the fundamental
property of equality preservation cannot be established. Our insight is
that just as one uses parametricity to restrict definable elements of a
type\, one can use parametricity of proofs to ensure equality
preservation. The idea of parametricity for proofs can be formalised
using the idea of 2-dimensional logical relations. Interestingly\, these
2-dimensional relations have clear higher dimensional analogues where
(n+1)-relations are fibered over a n-cube of n-relations. Thus the story
of proof relevant logical relations quickly expands into one of higher
dimensional structures similar to the cubical sets which arises in
Homotopy Type Theory. Of course\, there are also connections to Bernardy
and Moulin's work on internal parametricity.\n
UID:43
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150508T150000
DTEND;TZID=Europe/London:20150508T160000
LOCATION:LT1415
SUMMARY:Departmental seminar: The probability of the Alabama paradox
DESCRIPTION:Speaker: Svante Linusson (KTH\, Stockholm)\nTitle: The
probability of the Alabama paradox\n\nThere exists various possible
methods to distribute seats proportionally between states (or parties) in
a parliament. Hamilton's method (also known as the method of largest
reminder) was abandoned in the USA because of some drawbacks\, in
particular the possibility of the Alabama paradox\, but it is still in
use in many other countries.\n\nIn recent work (joint with Svante Janson)
we give\, under certain assumptions\, a closed formula for the
probability that the Alabama paradox occurs given the vector p_1,...,p_m
of relative sizes of the states.\n\nFrom the theorem we deduce a number
of consequences. For example it is shown that the expected number of
states that will suffer from the Alabama paradox is asymptotically
bounded above by 1/e. For random (uniformly distributed) relative sizes
p_1,...,p_m the expected number of states to suffer from the Alabama
paradox converges to slightly more than a third of this\, or
approximately 0.335/e=0.123\, as m -> infinity.\n\n I will assume no
prior knowledge of electoral mathematics\, but begin by giving a brief
background to various methods suggested and used for the distribution of
seats proportionally in a parliament (it's all in the rounding).\n
UID:42
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150506T110000
DTEND;TZID=Europe/London:20150506T120000
LOCATION:LT1310
SUMMARY:Game theory in string diagrams
DESCRIPTION:Speaker: Jules Hedges (Queen Mary University of
London)\nTitle: Game theory in string diagrams\n\nWe define a category
whose morphisms are 'games relative to a continuation'\, designed to
allow games to be built recursively from simple components. The resulting
category has interesting structure similar to (but weaker than) compact
closed\, and comes with an associated string diagram language.\n
UID:41
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150429T110000
DTEND;TZID=Europe/London:20150429T120000
LOCATION:LT1310
SUMMARY:An Introduction to Differential Privacy
DESCRIPTION:Speaker: Bob Atkey (MSP)\nTitle: An Introduction to
Differential Privacy\n\nLet's say you have a database of people's private
information. For SCIENCE\, or some other reason\, you want to let third
parties query your data to learn aggregate information about the people
described in the database. However\, you have a duty to the people whose
information your database contains not to reveal any of their individual
personal information. How do you determine which queries you will let
third parties execute\, and those you will not?\n\n"Differential Privacy"
defines a semantic condition on probabilistic queries that identifies
queries that are safe to execute\, up to some "privacy budget".\n\nI'll
present the definition of differential privacy\, talk a bit about why it
is better than some 'naive' alternatives (e.g.\, anonymisation)\, and
also describe how the definition can be seen as an instance of relational
parametricity.\n\nA good place to read about the definition of
differential privacy is the book "The Algorithmic Foundations of
Differential Privacy" by Cynthia Dwork and Aaron Roth.\n
UID:40
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150320T150000
DTEND;TZID=Europe/London:20150320T160000
LOCATION:LT1415
SUMMARY:Departmental seminar: Approximating transition systems
DESCRIPTION:Speaker: Chris Heunen (Oxford)\nTitle: Approximating
transition systems\n\nClassical computation\, invertible computation\,
probabilistic computation\, and quantum computation\, form increasingly
more sophisticated labelled transition systems. How can we approximate a
transition system by less sophisticated ones? Considering all ways to get
probabilistic information out of a quantum system leads to
domain-theoretic ideas\, that also apply in the accompanying Boolean
logic. I will survey to what extent these domains characterise the
system\, leading with examples from quantum theory\, in a way that is
accessible to a broad audience of computer scientists\, mathematicians\,
and logicians.\n
UID:39
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150429T150000
DTEND;TZID=Europe/London:20150429T160000
LOCATION:LT1415
SUMMARY:Departmental seminar: Cyclic homology from mixed distributive
laws
DESCRIPTION:Speaker: Uli Kraehmer (University of Glasgow)\nTitle: Cyclic
homology from mixed distributive laws\n\nIn pure mathematics\, cyclic
homology is an invariant of associative algebras that is motivated by
algebra\, topology and even mathematicial physics. However\, when studied
from an abstract point of view it turns out to be an invariant of a pair
of a monad and a comonad that are related by a mixed distributive law\,
and I speculate that this could lead to some potential applications in
computer science.\n\n(based on joint work with Niels Kowalzig and Paul
Slevin)\n
UID:38
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150422T140000
DTEND;TZID=Europe/London:20150422T150000
LOCATION:LT1310
SUMMARY:Patterns to avoid: (dependent) stringly-typed programming
DESCRIPTION:Speaker: Guillaume Allais (MSP)\nTitle: Patterns to avoid:
(dependent) stringly-typed programming\n\nType : Set\nType = String ->
Bool\n
UID:37
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150311T110000
DTEND;TZID=Europe/London:20150311T120000
LOCATION:LT1310
SUMMARY:Collapsing
DESCRIPTION:Speaker: Peter Hancock \nTitle: Collapsing\n\nThe topic comes
from theory of infinitary proofs\, and cut-elimination. In essence it is
about nicely-behaved maps from higher "infinities" to lower ones\, as the
infinitary proofs are er\, infinite\, and can be thought of as glorified
transfinite iterators. What might nice behaviour mean?\n\nYou can think
of it as how to fit an uncountable amount of beer into a bladder whose
capacity is merely countable. (Or maybe even finite.)\n\nThe most
ubiquitous form of infinity is the regular cardinal\, iepassing from a
container F to F + (mu F -> _)\, where mu is the W-type operation. I'll
"explain" regular collapsing as being all about diagonalisation.\n\n\n
UID:36
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150304T140000
DTEND;TZID=Europe/London:20150304T150000
LOCATION:LT1415
SUMMARY:Event: A HoTT-Date with Thorsten Altenkirch
DESCRIPTION:
UID:35
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150218T120000
DTEND;TZID=Europe/London:20150218T130000
LOCATION:Royal College Building\, room RC512
SUMMARY:Event: SPLS @ Strathclyde
DESCRIPTION:
UID:34
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150211T110000
DTEND;TZID=Europe/London:20150211T120000
LOCATION:LT1415
SUMMARY:Totality versus Turing Completeness?
DESCRIPTION:Speaker: Conor McBride (MSP)\nTitle: Totality versus Turing
Completeness?\n\nI gave an SPLS talk
(http://www.dcs.gla.ac.uk/research/spls/Mar12/)\, which was mostly
propaganda\, about why people should stop claiming that totality loses
Turing completeness. There was some technical stuff\, too\, about
representing a recursive definition as a construction in the free monad
whose effect is calling out to an oracle for recursive calls: that tells
you what it is to be recursive without prejudicing how to run it. I'm
trying to write this up double-quick as a paper for the miraculously
rubbery MPC deadline\, with more explicit attention to the monad
morphisms involved. So I'd be grateful if you would slap down the shtick
and make me more morphic. The punchline is that the Bove-Capretta domain
predicate construction is a (relative) monad morphism from the free monad
with a recursion oracle to the (relative) monad of Dybjer-Setzer
Induction-Recursion codes. But it's worth looking at other monad
morphisms (especially to the Delay monad) along the way.\n
UID:33
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150128T163000
DTEND;TZID=Europe/London:20150128T173000
LOCATION:LT1415
SUMMARY:Runners for your computations
DESCRIPTION:Speaker: Tarmo Uustalu (Institute of Cybernetics\,
Tallinn)\nTitle: Runners for your computations\n\nWhat structure is
required of a set so that computations in a given notion of computation
can be run statefully this with set as the state space? Some answers: To
be able to serve stateful computations\, a set must carry the structure
of a lens\; for running interactive I/O computations statefully\, a
"responder-listener" structure is necessary etc. I will observe that\, in
general\, to be a runner of computations for an algebraic theory (defined
as a set equipped with a monad morphism between the corresponding monad
and the state monad for this set) is the same as to be a comodel of this
theory\, ie a coalgebra of the corresponding comonad. I will work out a
number of instances. I will also compare runners to handlers.\n
UID:32
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20150122T110000
DTEND;TZID=Europe/London:20150122T120000
LOCATION:LT1310
SUMMARY:Termination\, later
DESCRIPTION:Speaker: James Chapman (Institute of Cybernetics\,
Tallinn)\nTitle: Termination\, later\n\nIt would be a great shame if
dependently-typed programming (DTP) restricted us to only writing very
clever programs that were a priori structurally recursive and hence
obviously terminating. Put another way\, it is a lot to ask of the
programmer to provide the program and its termination proof in one go\,
programmers should also be supported in working step-by-step. I will show
a technique that lowers the barrier of entry\, from showing termination
to only showing productivity up front\, and then later providing the
opportunity to show termination (convergence). I will show an example of
a normaliser for STLC represented in Agda as a potentially
non-terminating but nonetheless productive corecursive function targeting
the coinductive delay monad.\n\n(Joint work with Andreas Abel)\n
UID:31
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141217T110000
DTEND;TZID=Europe/London:20141217T120000
LOCATION:LT1310
SUMMARY:Worlds\, Types and Quantification
DESCRIPTION:Speaker: Conor McBride (MSP)\nTitle: Worlds\, Types and
Quantification\n\nI've managed to prove a theorem that I've been chasing
for a while. The trouble\, of course\, was *stating* it. I'll revisit the
motivation for extending type systems with an analysis of not just *what*
things are but *where*\, *when*\, *whose*\, etc. The idea is that typed
constructions occur in one of a preordered set of worlds\, with scoping
restricted so that information flows only "upwards" from one world to
another. Worlds might correspond to "at run time" and "during
typechecking"\, or to computation in distinct cores\, or in different
stages\, etc. What does the dependent function space mean in this
setting? For a long time\, I thought that each world had its own
universal quantifier\, for abstracting over stuff from that world.
Failure to question this presumption is what led to failure to state a
theorem I could prove. By separating quantifiers from worlds\, I have
fixed the problem. I'll show how to prove the key fact: if I can build
something in one world and then move it to another\, then it will also be
a valid construction once it has arrived at its destination.\n
UID:30
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141210T110000
DTEND;TZID=Europe/London:20141210T120000
LOCATION:LT1310
SUMMARY:ZX and PROPs
DESCRIPTION:Speaker: Aleks Kissinger (Oxford)\nTitle: ZX and PROPs\n\n\n
UID:29
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141203T140000
DTEND;TZID=Europe/London:20141203T150000
LOCATION:LT1310
SUMMARY:Event: HoTT reading group @ Strathclyde
DESCRIPTION:We will read the paper A Model of Type Theory in Cubical Sets
(http://drops.dagstuhl.de/opus/volltexte/2014/4628/pdf/7.pdf) by Marc
Bezem (http://www.ii.uib.no/~bezem/)\, Thierry Coquand
(http://www.cse.chalmers.se/~coquand/) and Simon Huber
(http://www.cse.chalmers.se/~simonhu/). Thierry's Variation on cubical
sets (http://www.cse.chalmers.se/~coquand/comp.pdf) might also be useful.
*Administrative details*: meet for lunch at 12am for those who want to\,
reading group starts at 2pm.
UID:28
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141119T120000
DTEND;TZID=Europe/London:20141119T130000
LOCATION:LT1310
SUMMARY:Arrow's Theorem and Escalation
DESCRIPTION:Speaker: Neil Ghani and Clemens Kupke (MSP)\nTitle: Arrow's
Theorem and Escalation\n\nNeil and Clemens will report back from the
Lorentz Center Workshop on Logics for Social Behaviour
(http://www.cs.le.ac.uk/people/akurz/lsb.html).\n
UID:27
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141126T110000
DTEND;TZID=Europe/London:20141126T120000
LOCATION:LT1310
SUMMARY:Diagrammatic languages for monoidal categories
DESCRIPTION:Speaker: Ross Duncan (MSP)\nTitle: Diagrammatic languages for
monoidal categories\n\nMonoidal categories are essentially 2-dimensional
things\, so why on earth would we represent them using a linear string of
symbols? I'll talk about how to use string diagrams for monoidal
categories\, graph rewriting for reasoning within them\, and how the
syntax can be extended to handle certain kinds of infinitary expressions
with the infamous !-box. If there's time I'll finish with some half-baked
(eh... basically still looking for the on switch of the oven...) ideas of
how to generalise them.\n
UID:26
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141106T090000
DTEND;TZID=Europe/London:20141106T100000
LOCATION:LT1310
SUMMARY:Comonadic Cellular Automata
DESCRIPTION:Speaker: Kevin Dunne (MSP)\nTitle: Comonadic Cellular
Automata\n\nKevin will be giving an informal talk about some of the stuff
he has been learning about. He'll give the definition of a cellular
automaton and then talk about how this definition can be phrased in terms
of a comonad.\n
UID:25
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141105T110000
DTEND;TZID=Europe/London:20141105T120000
LOCATION:Boardroom (LT1101d)
SUMMARY:Logical Relations for Monads by Categorical TT-Lifting
DESCRIPTION:Speaker: Shin-ya Katsumata (Kyoto University)\nTitle: Logical
Relations for Monads by Categorical TT-Lifting\n\nLogical relations are
widely used to study various properties of typed lambda calculi. By
extending them to the lambda calculus with monadic types\, we can gain
understanding of the properties on functional programming languages with
computational effects. Among various constructions of logical relations
for monads\, I will talk about a categorical TT-lifting\, which is a
semantic analogue of Lindley and Stark's leapfrog method.\n\nAfter
reviewing some fundamental properties of the categorical TT-lifting\, we
apply it to the problem of relating two monadic semantics of a
call-by-value functional programming language with computational effects.
This kind of problem has been considered in various forms: for example\,
the relationship between monadic style and continuation passing style
representations of call-by-value programs was studied around '90s. We
give a set of sufficient conditions to solve the problem of relating two
monadic semantics affirmatively. These conditions are applicable to a
wide range of such problems.\n
UID:24
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141027T140000
DTEND;TZID=Europe/London:20141027T150000
LOCATION:Boardroom (LT1101d)
SUMMARY:Constructing analysis-directed semantics
DESCRIPTION:Speaker: Dominic Orchard (Imperial College London)\nTitle:
Constructing analysis-directed semantics\n\nAll kinds of semantics are
syntax directed: the semantics follows from the syntax. Some varieties of
semantics are syntax and type directed. In this talk\, I'll discuss
syntax\, type\, *and* analysis directed semantics (analysis-directed
semantics for short!)\, for analyses other than types. An
analysis-directed semantics maps from terms coupled with derivations of a
static program analysis into some semantic domain. For example\, the
simply-typed lambda calculus with an effect system maps to the category
generated by a strong parametric effect monad (due to Katsumata) and a
bounded-linear logic-like analysis (described as a coeffect systems) maps
to a category generated by various structures related to monoidal
comonads. I'll describe a general technique for building
analysis-directed semantics where semantic objects and analysis objects
have the same structure and are coupled by lax homomorphisms between
them. This aids proving semantic properties: the proof tree of an
equality for two program analyses implies the rules needed to prove
equality of the programs' denotations.\n
UID:23
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141112T110000
DTEND;TZID=Europe/London:20141112T120000
LOCATION:LT1310
SUMMARY:Lambda-abstraction and other diabolical contrivances
DESCRIPTION:Speaker: Peter Hancock \nTitle: Lambda-abstraction and other
diabolical contrivances\n\nThe topic is the unholy trinity of eta\,
zeta\, and xi. I'll indicate how Curry managed to give a finite
combinatorial axiomatisation of this nastiness\, by anticipating
(almost-but-not-*quite*) McBride et al's applicative functors.\n
UID:22
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141029T120000
DTEND;TZID=Europe/London:20141029T130000
LOCATION:Dundee
SUMMARY:Event: SICSA CSE Meeting on Effects and Coeffects Systems and
their use for resource control
DESCRIPTION:
UID:21
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141022T110000
DTEND;TZID=Europe/London:20141022T120000
LOCATION:LT1310
SUMMARY:Higher dimensional parametricity and its cubical structure
DESCRIPTION:Speaker: Neil Ghani (MSP)\nTitle: Higher dimensional
parametricity and its cubical structure\n\nNeil will talk about partial
progress made during the summer on higher dimensional parametricity and
the cubical structures that seem to arise. \nDetails will be kept to a
minimum and\, of course\, concepts stressed.\n
UID:20
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141015T120000
DTEND;TZID=Europe/London:20141015T130000
LOCATION:Heriot Watt
SUMMARY:Event: SPLS
DESCRIPTION:
UID:19
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141008T110000
DTEND;TZID=Europe/London:20141008T120000
LOCATION:LT1310
SUMMARY:"Real-world data" and dependent types
DESCRIPTION:Speaker: Conor McBride (MSP)\nTitle: "Real-world data" and
dependent types\n\nConor has offered to talk to us about what he has been
thinking about recently. He says this includes models\, views\, and
dependent types.\n
UID:18
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20141001T110000
DTEND;TZID=Europe/London:20141001T120000
LOCATION:LT1310
SUMMARY:Initial algebras via strong dinaturality\, internally
DESCRIPTION:Speaker: Fredrik Nordvall Forsberg (MSP)\nTitle: Initial
algebras via strong dinaturality\, internally\n\n Or: My summer with
Steve\nOr: How Christine and Frank were right\, after all\nOr: Inductive
types for the price of function extensionality and impredicative Set\n\n
Christine Paulin-Mohring and Frank Pfenning suggested to use
impredicative encodings of inductive types in the Calculus of
Constructions\, but this was later abandoned\, since it is "well-known"
that induction principles\, i.e. dependent elimination\, can not be
derived for this encoding. It now seems like it is possible to give a
variation of this encoding for which the induction principle is derivable
after all. The trick is to use identity types to cut down the
transformations of type (Pi X : Set) . (F(X) -> X) -> X to the ones that
are internally strongly dinatural\, making use of a formula for a
"generalised Yoneda Lemma" by Uustalu and Vene.\n
UID:17
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140815T150000
DTEND;TZID=Europe/London:20140815T160000
LOCATION:LT1310
SUMMARY:Internal parametricity
DESCRIPTION:Speaker: Fredrik Nordvall Forsberg (MSP)\nTitle: Internal
parametricity\n\n\n
UID:16
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140528T110000
DTEND;TZID=Europe/London:20140528T120000
LOCATION:LT1310
SUMMARY:Graphical algebraic foundations for monad stacks
DESCRIPTION:Speaker: Ohad Kammar (Cambridge)\nTitle: Graphical algebraic
foundations for monad stacks\n\nOhad gave an informal overview of his
current draft\, with the following abstract:\n\nHaskell incorporates
computational effects modularly using sequences of monad transformers\,
termed monad stacks. The current practice is to find the appropriate
stack for a given task using intractable brute force and heuristics. By
restricting attention to algebraic stack combinations\, we provide a
linear-time algorithm for generating all the appropriate monad stacks\,
or decide no such stacks exist. Our approach is based on Hyland\,
Plotkin\, and Power's algebraic analysis of monad transformers\, who
propose a graph-theoretical solution to this problem. We extend their
analysis with a straightforward connection to the modular decomposition
of a graph and to cographs\, a.k.a. series-parallel graphs.\n\nWe present
an accessible and self-contained account of this monad-stack generation
problem\, and\, more generally\, of the decomposition of a combined
algebraic theory into sums and tensors\, and its algorithmic solution. We
provide a web-tool implementing this algorithm intended for semantic
investigations of effect combinations and for monad stack generation.\n
UID:15
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140521T110000
DTEND;TZID=Europe/London:20140521T120000
LOCATION:LT1310
SUMMARY:Coalgebraic Foundations of Databases
DESCRIPTION:Speaker: Clemens Kupke (MSP)\nTitle: Coalgebraic Foundations
of Databases\n\n This 101 is intended to be a brainstorming session on
possible links between the theory of coalgebras and the theory of
databases. I will outline some ideas in this direction and I am looking
forward to your feedback.\n
UID:14
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140514T110000
DTEND;TZID=Europe/London:20140514T120000
LOCATION:LT1310
SUMMARY:Resource aware contexts and proof search for IMLL
DESCRIPTION:Speaker: Guillaume Allais (MSP)\nTitle: Resource aware
contexts and proof search for IMLL\n\nIn Intuitionistic Multiplicative
Linear Logic\, the right introduction rule for tensors implies picking a
2-partition of the set of assumptions and use each component to inhabit
the corresponding tensor's subformulas. This makes a naive proof search
algorithm intractable. Building a notion of resource availability in the
context and massaging the calculus into a more general one handling both
resource consumption and a notion of "leftovers" of a subproof allows for
a well-structured well-typed by construction proof search mechanism.\n\n
Here is an Agda file
(http://gallais.org/code/LinearProofSearch/poc.LinearProofSearch.html)
implementing the proof search algorithm.\n
UID:13
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140407T110000
DTEND;TZID=Europe/London:20140407T120000
LOCATION:LT1310
SUMMARY:Nominal sets
DESCRIPTION:Speaker: Jamie Gabbay (Heriot-Watt)\nTitle: Nominal
sets\n\n\n
UID:12
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140402T110000
DTEND;TZID=Europe/London:20140402T120000
LOCATION:LT1310
SUMMARY:Towards cubical type theory
DESCRIPTION:Speaker: Thorsten Altenkirch (Nottingham)\nTitle: Towards
cubical type theory\n\n\n
UID:11
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140319T110000
DTEND;TZID=Europe/London:20140319T120000
LOCATION:LT1310
SUMMARY:The selection monad transformer
DESCRIPTION:Speaker: Guillaume Allais (MSP)\nTitle: The selection monad
transformer\n\nGuillaume presented parts of Hedges' paper Monad
transformers for backtracking search
(http://www.eecs.qmul.ac.uk/~julesh/papers/monad_transformers.pdf)
(accepted to MSFP 2014 (http://www.cs.bham.ac.uk/~pbl/msfp2014/)). The
paper extends Escardo and Oliva's work on the selection and continuation
monads to the corresponding monad transformers\, with applications to
backtracking search and game theory.\n
UID:10
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140305T150000
DTEND;TZID=Europe/London:20140305T160000
LOCATION:LT1310
SUMMARY:Lagrange inversion
DESCRIPTION:Speaker: Stuart Hannah (Strathclyde Combinatorics)\nTitle:
Lagrange inversion\n\nStuart spoke about Lagrange inversion\, a
species-theoretic attempt to discuss the existence of solutions to
equations defining species.\n
UID:9
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140228T140000
DTEND;TZID=Europe/London:20140228T150000
LOCATION:LT1310
SUMMARY:Species
DESCRIPTION:Speaker: Neil Ghani (MSP)\nTitle: Species\n\nNeil spoke about
how adding structured quotients to containers gives rise to a larger
class of data types.\n
UID:8
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140219T110000
DTEND;TZID=Europe/London:20140219T120000
LOCATION:LT1310
SUMMARY:Synthetic Differential Geometry
DESCRIPTION:Speaker: Tim Revell (MSP)\nTitle: Synthetic Differential
Geometry\n\nTim gave a brief introduction to Synthetic Differential
Geometry. This is an attempt to treat smooth spaces categorically so we
can extend the categorical methods used in the discrete world of computer
science to the continuous work of physics. \n
UID:7
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140212T110000
DTEND;TZID=Europe/London:20140212T120000
LOCATION:LT1310
SUMMARY:Worlds
DESCRIPTION:Speaker: Conor McBride (MSP)\nTitle: Worlds\n\nConor talked
about worlds (aka phases\, aka times\, ...): why one might bother\, and
how we might go about equipping type theory with a generic notion of
permitted information flow.\n
UID:6
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140205T110000
DTEND;TZID=Europe/London:20140205T120000
LOCATION:LT1310
SUMMARY:Operads
DESCRIPTION:Speaker: Miles Gould (Edinburgh)\nTitle: Operads\n\nMiles has
kindly agreed to come through and tell us about Operads\, thus revisiting
the topic of his PhD and the city in which he did it. \n
UID:5
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140122T110000
DTEND;TZID=Europe/London:20140122T120000
LOCATION:LT1310
SUMMARY:Overview of (extensions of) inductive-recursive definitions
DESCRIPTION:Speaker: Lorenzo Malatesta (MSP)\nTitle: Overview of
(extensions of) inductive-recursive definitions\n\n\n
UID:4
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20140108T110000
DTEND;TZID=Europe/London:20140108T120000
LOCATION:LT1310
SUMMARY:On the recently found inconsistency of the univalence axiom in
current Agda and Coq
DESCRIPTION:Speaker: Conor McBride (MSP)\nTitle: On the recently found
inconsistency of the univalence axiom in current Agda and Coq\n\n\n
UID:3
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20131218T110000
DTEND;TZID=Europe/London:20131218T120000
LOCATION:LT1310
SUMMARY:Quantum Mechanics
DESCRIPTION:Speaker: Ross Duncan (MSP)\nTitle: Quantum Mechanics\n\n\n
UID:2
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20131120T110000
DTEND;TZID=Europe/London:20131120T120000
LOCATION:LT1310
SUMMARY:Classical Type Theories
DESCRIPTION:Speaker: Robin Adams (MSP visitor)\nTitle: Classical Type
Theories\n\nIn 1987\, Felleisen showed how to add control operators (for
things like exceptions and unconditional jumps) to the untyped
lambda-calculus. In 1990\, Griffin idly wondered what would happen if one
did the same in a typed lambda calculus. The answer came out: the
inhabited types become the theorems of classical logic.\n\n I will
present the lambda mu-calculus\, one of the cleanest attempts to add
control operators to a type theory. We'll cover the good news: the
inhabited types are the tautologies of minimal classical logic\, and
Godel's Double Negation translation from classical to intuitionistic
logic turns into the CPS translation.\n\nAnd the bad news: control
operators don't play well with other types. Add natural numbers (or some
other inductive type)\, and you get inconsistency. Add Sigma-types\, and
you get degeneracy (any two objects of the same type are definitionally
equal). It gets worse: add plus-types\, and you break Subject
Reduction.\n
UID:1
END:VEVENT
BEGIN:VEVENT
DTSTAMP;TZID=Europe/London:20180816T171005
DTSTART;TZID=Europe/London:20131113T110000
DTEND;TZID=Europe/London:20131113T120000
LOCATION:LT1310
SUMMARY:Continuation Passing Style
DESCRIPTION:Speaker: Guillaume Allais (MSP)\nTitle: Continuation Passing
Style\n\nI chose to go through (parts of) Hatcliff and Danvy's paper "A
Generic Account of Continuation-Passing Styles"
(http://dl.acm.org/citation.cfm?id=178053) (POPL 94) which gives a nice
factorization of various CPS transforms in terms of: \n * embeddings from
STLC to Moggi's computational meta-language (either call-by-value\,
call-by-name\, or whatever you can come up with)\n * followed by a
generic CPS transform transporting terms from ML back to STLC\n Here is
an Agda file (http://gallais.org/code/GenericCPS/definitions.html)
containing what we had the time to see.\n
UID:0
END:VEVENT
END:VCALENDAR