=20
**=20
**

=20

=20
=20

=20
=20

=20
Seminar series of the Mathematical Foundations group at the University o= f Bath.

Tuesdays 13:15 - 15:05 in 1W 2.104

Seminars are open to all.

=20

=20
=20

=20
Organisers: Willem Heijltjes and Giulio Guerrieri

Email us to suggest speakers

=20

=20
=20

=20
=20

=20
**Upcoming seminars**

**16th April**

**Alessio Santamaria (University of Bath)**

Towards a Godement Calculus for Dinatural Transfo= rmations

Dinatural transformations, which have been used to = interpret the second-order lambda calculus [1] as well as derivations in in= tuitionistic logic [2] and multiplicative linear logic [3], fail to compose= in general; this has been known since they were discovered by Dubuc and St= reet in 1970 [4]. Many ad hoc solutions to this remarkable shortcoming have= been found, but a general theory of compositionality was missing. The resu= lts Guy and I obtained during my PhD and that I=E2=80=99ll show in the talk= are the following: =

1. = Acycli= city of certain graphs associated to dinatural transformations is a suffici= ent and essentially necessary condition for two dinatural transformations t= o compose;

2. = This y= ields to the definition of a category whose objects are mixed-variant funct= ors and morphisms are partially dinatural transformations;

3. = A new = definition of horizontal composition for dinatural transformations embodyin= g substitution of functors into transformations and vice-versa, intuitively= reflected from the string-diagram point of view by substitution of graphs = into graphs.

This work represents the first,=
fundamental steps towards a Godement-like calculus of dinatural transforma=
tions as sought=E2=80=94but never achieved=E2=80=94by Kelly in [5], with th=
e intention then to apply it to describe coherence problems abstractly [6].=
We have not managed to get such a complete calculus yet, but we are =E2=80=
=9Cwell on our way=E2=80=9D on the path paved by Kelly himself in [5] when =
he was assessing the simpler case of a many-variable __fully covariant__=
functorial calculus. What we have not done yet will be the subject of futu=
re work.

[1] Bainbridge, E.S., Freyd, P.=
J., Scedrov, A. and Scott, P.J., 1990. Functorial polymorphism. *Theoret=
ical Computer Science* [Online], 70(1), pp.35=E2=80=9364. Available fro=
m: https://doi.org/10.1016/0304-3975(90)90151-7=
.

[2] Girard, J.-Y., Scedrov, A. =
and Scott, P.J., 1992. Normal Forms and Cut-Free Proofs as Natural Transfor=
mations. In: N.M. Yiannis, ed. *Logic from Computer Science*, [Onlin=
e]. Mathematical Sciences Research Institute Publications. Springer, New Yo=
rk, NY, pp.217=E2=80=93241. Available from: https://d=
oi.org/10.1007/978-1-4612-2822-6_8.

[3] Blute, R., 1993. Linear log=
ic, coherence and dinaturality. *Theoretical Computer Science* [Onli=
ne], 115(1), pp.3=E2=80=9341. Available from: https=
://doi.org/10.1016/0304-3975(93)90053-V.

[4] Dubuc, E. and Street, R., 1=
970. Dinatural transformations. In: S. Mac Lane, H. Applegate, M. Barr, B. =
Day, E. Dubuc, A.P. Phreilambud, R. Street, M. Tierney and S. Swierczkowski=
, eds. *Reports of the Midwest Category Seminar IV*, [Online]. Lectu=
re Notes in Mathematics. Springer, Berlin, Heidelberg, pp.126=E2=80=93137. =
Available from: https://doi.org/10.1007/BFb0060443.=

[5] Kelly, G.M., 1972. Many-var=
iable functorial calculus. I. In: G.M. Kelly, M. Laplaza, G. Lewis and S. M=
ac Lane, eds. *Coherence in Categories*, [Online]. Lecture Notes in =
Mathematics. Springer, Berlin, Heidelberg, pp.66=E2=80=93105. Available fro=
m: https://doi.org/10.1007/BFb0059556.

[6] Kelly, G.M., 1972. An abstr=
act approach to coherence. In: G.M. Kelly, M. Laplaza, G. Lewis and S. Mac =
Lane, eds. *Coherence in Categories*, [Online]. Lecture Notes in Mat=
hematics. Springer, Berlin, Heidelberg, pp.106=E2=80=93147. Available from:=
https://doi.org/10.1007/BFb0059557.

=20

=20
=20

=20
=20

=20
**Past seminars**

=20
**=20
**

=20
**=20
**

=20
**
**

In this talk we will detail how several generalisations and

extensions of this interpretation arguably form a basis for a

logical foundation that captures several interesting features of

message-passing concurrent computation. Specifically, we will

detail how the basic interpretation can be extended to richer

typed settings such as polymorphism and dependent type theories

and how to account for a meaningful notion of typed process

equivalence that gives meaning to both proof conversions and type

isomorphisms.
**
****
****
****
****
****From finitary monads to Lawvere theories: Cauchy completion=
s**
**(joint with Richard Garner)**
**The two main category theoretic formulations of universal algebra a=
re Lawvere theories and finitary (=3D filtered-colimit preserving) monads o=
n Set. The usual way in which to construct a Lawvere theory from a finitary=
monad T is by considering the opposite of the restriction of the=
Kleisli category Kl(T) to finite sets or equivalently natural numbers. Ric=
hard Garner recently found a different formulation of this, using the =
notion of Cauchy completion of a finitary monad qua monoid, =
i.e., qua one-object V-category, in V, where V is the monoidal categor=
y [Set_f,Set], equivalently the monoidal category [Set,Set]f of&n=
bsp;filtered-colimit preserving functors from Set to Set. **
**Both finitary monads (easily) and Lawvere theories (with more effor=
t) extend from Set to arbitrary locally finitely presentable categories. So=
last year in Sydney, Richard and I explored the extension of his construct=
ion via Cauchy completions. That works most naturally if one does it in a u=
nified way, i.e., not for one locally finitely presentable category at a ti=
me, but for all simultaneously, using the notion of W-category for a bicate=
gory W.**
**I shall talk about as much of this as we can reasonably handle: it =
is work in progress, so I have not fully grasped it myself yet, and there i=
s much to absorb, e.g, the concepts of Cauchy completion and categories enr=
iched in bicategories. The emphasis will very likely be on Richard's w=
ork rather than the work we did jointly. **
**Logic programming: laxness and saturation**
**(joint with Ekaterina Komendantskaya)**
**A propositional logic program P may be identified with a (Pf Pf)-co=
algebra on the set of atomic propositions in the program. The corresponding=
C(Pf Pf)-coalgebra, where C(Pf Pf) is the cofree comonad on Pf Pf, describ=
es derivations by resolution.That correspondence has been developed to mode=
l first-order programs in two ways, with lax semantics and saturated semant=
ics, based on locally ordered categories and right Kan extensions respectiv=
ely. We unify the two approaches, exhibiting them as complementary rather t=
han competing, reflecting the theorem-proving and proof-search aspects of l=
ogic programming.**

While maintaining that unity, we further refine lax semantics t= o give finitary models of logic progams with existential variables, and to = develop a precise semantic relationship between variables in logic programm= ing and worlds in local state.
**Our work is not yet complete, but we believe it explicate=
s at least part of the underlying structure more clearly than hitherto=
done by using an enriched category theoretic perspective**
**
****
****
****
****
****
****
****
****
****
****
****
****
****
**

**
****
****
****
****
****
****
****
****
****
****
****
****
****
****
**

__2019__

**19th March**

**Nicolas Wu (University of Bristol)**

The Scope= of Algebraic Effect Handlers

Algebraic effect handlers are a methodology for dealing with effectful p= rograms in a modular way. They build on the free monad for a functor as mea= ns of describing a syntax tree. An interpretation of syntax is provided by = a handler, which folds over the structure with an algebra. Handlers themsel= ves are not always algebraic operations, which can lead to surprising prope= rties of programs written in this style. This talk presents scoped algebrai= c effect handlers, which allow a certain class of handlers to be expressed = algebraically.

**12th March**

**Luc Pellissier (Universit=C3=A9 Paris Diderot)**)<=
/span>

Fibrations, approximations and intersection type syst= ems (joint work with Damiano Mazza and<= strong> Pierre Vial

We present calculi (intuitionistic or classical) in a= bioperadic setting, and, following Melli=C3=A8s and Zeilberger (2015), rep= resent type systems as morphisms of such structure.

Programs in such calculi can be approximated arbitrar= ily well by linear programs, that use their argument exactly once. In this = work, we show that such linear approximations give rise, through an adapted= Grothendieck construction, to intersection type systems for any logical sy= stem that can be embed meaningfully into linear logic.

We recover in this way all well-known intersection ty= pe systems, capturing different notions of normalization for various langua= ges, and give a blueprint to compute new ones.

**26th February**

**Willem Heijltjes (University of Bath)** (joint work with

Intuit= ionistic Proofs without Syntax

Hughes's Combinatorial Proofs are an intriguing, purely graphical notion= of proof for propositional classical logic. Here, we answer the question: = what is their intuitionistic counterpart? Our result, Intuitionistic Combin= atorial Proofs (ICPs), are a concrete geometric semantics of intuitionistic= proof that reveal many interesting connections: to game semantics, deep in= ference, supercombinator reduction, and more.

The technical development starts with a graphical representation of form= ulas, in the style of arenas in game semantics, and co-graphs and coherence= spaces in classical and linear logic. Unlike game semantics, where arenas = are most often tree-like, our arenas are DAG-like.

ICPs, like their classical counterparts, are then composed of two fragme= nts: a linear fragment called an "arena net", and a contraction-weakening f= ragment called a "skew fibration". An arena net is a proof net in intuition= istic multiplicative linear logic (IMLL), but over an arena rather than a f= ormula. A skew fibration is a particular graph homomorphism between the are= na net and the arena for the conclusion formula of the proof.

In contrast with linear logic, where linear/non-linear factorization is = at the formula level through the bang operator, ICPs factor at the level of= proofs, like Herbrand's Theorem for first-order classical logic, and like = proof stratification in deep inference. An ICP can be viewed as a Hyland-On= g strategy with additional sharing.

ICPs abstract fully and faithfully over all non-duplicating permutations= of the sequent calculus, a result we call "Polynomial Full Completeness" t= hat is analogous to the Hughes and Heijltjes's recent "Local Canonicity" re= sult for MALL. By contrast, lambda-calculus and game semantics incur an exp= onential blowup. This manifests in ICPs as a natural form of sharing, induc= ed by the DAG-form of arenas.

We give a simple and direct normalization relation that arises naturally= from the semantics. It relates to closed reduction in lambda-calculus (a r= edex may only reduce if it contains no free variables) and supercombinator = reduction (as used in the implementation of Haskell), techniques originally= devised for reasons of efficiency. Intriguingly, the sharing in ICPs need = not be unfolded during normalization, and instead the shared subterm is eva= luated first, similarly to call-by-need reduction.

**12th February**

**David Sherratt (University of Bath)Explorin=
g the limits of full laziness**

For my PhD I introduce a variant of Gundersen, Heijltjes, and Pari= got's atomic lambda calculus. This typeable calculus with explicit sharing = extends the Curry-Howard interpretation of open deduction already establish= ed by the previous calculus. This expanded interpretation al= lows us to follow a duplication strategy stronger than full laziness, = in the sense that we duplicate less and share more of a term. We call this = optimal laziness, and explain the different levels of laziness and how they= relate to implementations, including optimal graph reduc= tion in the style of Lamping.

**15th January**

**Andrea Aler Tubella (University =
Paris Diderot)**

Decomposing proof systems with contracti= on

We present a general normalisation theory for logics with contraction. W=
e show that in a wide variety of proof systems fulfilling some general cond=
itions we can separate every proof into two phases: a linear phase followed=
by a phase made up only of contractions.

By combining these results tog=
ether with splitting, a generalised cut-elimination theory for linear proof=
systems, we are therefore presenting a modular normalisation theory encomp=
assing many existing logics.

__2018__

**20th November**

**Giulio Guerrieri (University of Bologna)Types of Fireballs **

The good properties of Plotkin's c= all-by-value lambda-calculus crucially rely on the restriction to weak eval= uation and closed terms. Open call-by-value is the more general setting whe= re evaluation is weak but terms may be open. Such an extension is delicate = and the literature contains a number of proposals. Recently, we provided op= erational and implementative studies of these proposals, showing that they = are equivalent with respect to termination, and also at the level of time c= ost models. This paper explores the denotational semantics of open call-by-= value, adapting de Carvalho's analysis of call-by-name via multi types (aka= non-idempotent intersection types). Our type system characterises normalis= ation and thus provides an adequate relational semantics. Moreover, type de= rivations carry quantitative information about the cost of evaluation: thei= r size bounds the number of evaluation steps and the size of the normal for= m, and we also characterise derivations giving exact bounds. The study cruc= ially relies on a new, refined presentation of the fireball calculus, the s= implest proposal for open call-by-value, that is more apt to denotational i= nvestigations.

**30th=
October**

**Georg Moser (University of Innsbruck)Epsilon Calculus and Herbrand Complexity (the case with equa=
lity)**

Hilbert's epsilon calculus is base=
d on an extension of the language of

predicate logic by a term-forming operator $\va=
repsilon_{x}$. Two

fundamental results about the epsilon calculus, the first a=
nd second

epsilon theorem, =
play a r\^ole similar to that which cut-elimination

<=
span style=3D"color: rgb(33,33,33);">or decomposition tec=
hniques in other logical formalisms.&nb=
sp; In

particular,&nb=
sp; Herbrand's Theorem is a consequence of&nb=
sp; the epsilon

theor=
ems. In the talk I will present the epsilon theorems and present

new results (for the =
; case with equality) on the complexity of the

=
elimination procedure underlying thei=
r proof, as well as the length of

Herbrand disjunctions of existential t=
heorems obtained by this

elimination procedure.

**13 June**

**James Davenport (University of Bath)**

Computer algebra systems started o= ff manipulating polynomials over the integers, or groups of permutations. A= s they moved into greater ranges of data structures, the need for underpinn= ing theory became felt, and Scratchpad II (later Axiom) was the first syste= m to use Universal Algebra and Category Theory for this. These days, = other systems such as Sage and Magma also do this. This Talk explains= how Axiom=E2=80=99s category structure works, and some of the challenges p= osed by constructivity.

**22 May**

**Fabio Zanasi (University College=
of London)**

Diagrammatic languages are used in diverse fields of science to specify=
and study systems based on interacting

components. Graphics outperforms textual information in highli=
ghting connectivity and resource-exchange between parts of

a system. This makes diagrammatic languages=
particularly effective in the analysis of subtle interactions as those fou=
nd in

cyber-physical, concu=
rrent and quantum systems.

In recent years "algebraic network theory" emerged in theoretical compu=
ter science as a unifying mathematical framework in which diagrammatic lang=
uages are given a completely formal status and are studied using the compos=
itional methods of algebraic program

semantics. Nowadays the algebraic approach founds application in =
fields as diverse as quantum theory, linguistics, Bayesian probability, con=
currency theory and the analysis of signal processing, electrical and digit=
al circuits.

In this talk I give a general overview of the approach, focussing on si= gnal processing theory as case study. Towards the end I will touch on some = current research threads, including structural operational semantics for st= ring diagrams, diagram rewriting implementation, and diagrammatic reasoning= in Bayesian inference.

**15 May**

**Joe Paulus (University of Bath)<=
br>****Deep Inference Intersec=
tion Types**

In this walk we investigate typing= the basic calculus, a linear calculus with explicit sharing. We do this in= open deduction formalism which is a combination of the sequent calculus an= d natural deduction. In the process we made the key innovation of multiset = derivations in open deduction.

**8 May**

**James Laird (University of Bath)=
**

Bounded quantification (exemplifie= d by the typing system Fsub) combines parametric polymorphism with subtypin= g, increasing its capacity to capture genericity and modularity of code by = representing phenomena such as inheritance.

We describe a denotational s=
emantics for bounded quantification, specifically:

- A general construction of a model of Fsub from a =
model of System F (the second order lambda-calculus) which has certain dina=
turality properties. (A "converse" to the observation of Cardelli et.=
al. that instantiation of bounded quantifiers should be dinatural in subty=
pe coercions.)

-A category =
of polymorphic games with the required dinaturality properties.

-A game semantics based on=
the above, for a programming language in which programs are stateful objec=
ts with bounded polymorphic types. In this model, full abstraction holds fo=
r "concretely bounded" types, but fails in general, arguably pointing to a =
gap in the expressiveness of existing typing systems for bounded polymorphi=
sm.

**20 March**

**Zak Tonks (University of Bath)****Fast Matrix Inversion in=
Computer Algebra**

James R. Bunch and John E. Hopcroft improved upon Strassen=E2=80=99s (19= 69) method for matrix inversion via fast matrix multiplication in 1974= . Bunch=E2=80=93Hopcroft handled the case in which principal submatrices ar= e singular, and presented a modi=EF=AC=81cation for providing LU factorisat= ion via this scheme. Such fast matrix multiplication techniques based on St= rassen=E2=80=99s method recurse via 7 multiplications on submatrices instea= d of the naive 8, and such methods achieve a worst case complexity of = O(n^=CF=89) where =CF=89 =3D log2 7.

However, Bunch=E2=80=93Hopcroft=E2=80=99s method assumes that the input = matrix is over a =EF=AC=81eld =E2=80=94 in particular the recursive nature = of the algorithm requires that certain elements and sub-determinants are in= vertible. But this is not always true of a ring, and in doing Computer Alge= bra we are most interested in rings of polynomials. In this presentation a = fraction free formulation of the algorithm is presented that is most suitab= le for (dense) matrices of sparse polynomials, where the intention is that = such a method should be more e=EF=AC=83cient than interpolation methods in = this case. In such a way, it is attempted to provide for these matrix inver= sion methods what Bareiss=E2=80=93Dodgson did for Gaussian Elimination.&nbs= p;

**9 January**

**Vladimir Dotsenko (Trinity Colle=
ge Dublin)**

The geometric notion of an F-manif= old was introduced by Hertling and Manin as a natural generalisation of the= celebrated notion of a Frobenius manifold. Pointwise, the structure of an = F-manifold leads to an algebraic structure on tangent spaces that is a weak= ened version of a Poisson algebra, that is a commutative associative produc= t and a Lie bracket that are compatible in some way that is slightly weaker= the Leibniz identity for Poisson algebras. Poisson algebras can be thought= of as "infinitesimal associative algebras". The slogan of this talk is tha= t "F-manifold algebras are infinitesimal pre-Lie algebras", relating them t= o a remarkable algebraic structure discovered independently by Gerstenhaber= , Koszul and Vinberg in the 1960s. I shall outline the proof, which relies = on a mixture of theory of rewriting systems and homotopical algebra.=

__2017__

**28 November**

**Nobuko Yoshida (Imperial College=
of London)**

In this talk, we first outline recent activities in our mobility gr= oup in

Department of Computing, Imperial College London.

Then we talk about the following work on Linear Logic and Session Types.&nb=
sp;

Linear logic has long been heralded as a potential model for

concurrency: from Girard's original paper, to Abramsky's

computational interpretation, reiterated by Bellin and

Scott. More recently, an interpretation for intuitionistic linear

logic has been given by Caires and Pfenning where propositions

are viewed as session types - a well established typing

discipline for concurrency - proofs as processes and proof

reduction as inter-process communication.

concurrency: from Girard's original paper, to Abramsky's

computational interpretation, reiterated by Bellin and

Scott. More recently, an interpretation for intuitionistic linear

logic has been given by Caires and Pfenning where propositions

are viewed as session types - a well established typing

discipline for concurrency - proofs as processes and proof

reduction as inter-process communication.

In this talk we will detail how several generalisations and

extensions of this interpretation arguably form a basis for a

logical foundation that captures several interesting features of

message-passing concurrent computation. Specifically, we will

detail how the basic interpretation can be extended to richer

typed settings such as polymorphism and dependent type theories

and how to account for a meaningful notion of typed process

equivalence that gives meaning to both proof conversions and type

isomorphisms.

**21 November**

**Hugo Paquet (University of Cambridge)**

Game semantics has been very succe= ssful at modelling the language PCF and various extensions. In particular, there is a fully abstract= games model (Danos-Harme= r 2002) for Probabilistic Algol, an extension of PCF with probability and ground references. But it = proved difficult to study Probabilistic PCF itself= , without references, in this context.

I will show how concurrent games, bas=
ed on event structures, provide a
new framework for probabilistic game =
semantics. In this setting we can
express "probabilistic innocence", th=
e property characterising
Probabilistic PCF programs. We will s=
ee that concurrent games also allow
us to also interpret a
concurrent version of Probabilistic P=
CF, in which
some programs can be evaluated in par=
allel. Finally, I will talk about a
new direction in probabilistic game s=
emantics, aiming at supporting
languages with continuous probability=
distributions.

**7 November**

**Pawel Sobocinski (University of Southampton)**

Graphical linear algebra is a string diagrammatic alternative to the usu= al mathematical treatment of linear algebra (vector spaces,= matrices and all that). Like process algebra, it is both a specificat= ion language and an implementation language, giving a new way "op= erational" way to approach this classical and uniquely important = mathematical subject. The language enjoys a sound and complete axiomatisati= on (called the theory of Interacting Hopf Algebras), making it an= attractive alternative calculus in which one can perform elementary&n= bsp;computations of linear algebra.

Finally, string diagrams=E2=80=93like classical syntax=E2=80=93can be eq= uipped with an operational semantics, becoming an extension Shann= on's signal flow graphs, connecting process algebraic notions with cla= ssical control and systems theory.

**31 October**

**Lutz Stra =C3=9Fburger (I=
NRIA Saclay - Ile de France**

In this talk I will introduce combina= torial flows as a generalization of Hughes' combinatorial proofs. I will show how they can cover cut an= d substitution as methods of= proof compression, and how cut and substitution are eliminated. Finally, I will show how proofs in syn= tactic formalisms like deep = inference or sequent calculus are translated into combinatorial flows and vice versa.

**7 June**

**Pierre Clairambault (ENS d=
e Lyon)**

Herbrand's theorem, often regarded=
as a cornerstone of proof theory, exposes some of the constructive co=
ntent of classical logic. In its simplest form, it reduces the validit=
y of a first-order purely

existential formula =E2=88=83x.=CF=86(x)=
(with =CF=86 quantifier-free) to that of a finite disjunction =CF=86(t=E2=
=82=81) =E2=88=A8 ... =E2=88=A8 =CF=86(t=E2=82=99). More generally, it give=
s an education of first-order validity to propositional validity, by&n=
bsp;understanding the structure of the assignment of first-order terms to&n=
bsp;existential quantifiers, and the causal dependency between quantifiers.=

In this talk, I will show that Her= brand's theorem in its general form can be elegantly stated as a theor= em in the framework of concurrent games. The causal structure of concu= rrent strategies, paired with annotations by first-order terms, is use= d to specify the dependency between quantifiers. Furthermore concurrent str= ategies can be composed, yielding a compositional proof of Herbrand's = theorem, simply by interpreting classical sequent proofs in a well-cho= sen denotational model. I assume no prior knowledge of Herbrand's theo= rem or concurrent games.

This is joint work with Aurore Alc= olei, Martin Hyland and Glynn Winskel.

**6 June**

**John Gowers (University of=
Bath)**

**The non-commutative sequoid operator =E2=8A=98 on games was intr=
oduced to capture algebraically the presence of state in history-sensitive =
strategies in game semantics, by imposing a causality relation on the tenso=
r product of games. Coalgebras for the functor A =E2=8A=98 _ - i.e., m=
orphisms from S to A =E2=8A=98 S - may be viewed as state transformers: if =
A =E2=8A=98 _ has a final coalgebra, !A, then the anamorphism of such a sta=
te transformer encapsulates its explicit state, so that it is shared only b=
etween successive invocations.**

**When we use this construction to model stateful objects in game =
semantics, we are using two properties of the game !A: firstly, that i=
t is the final coalgebra for the functor A =E2=8A=98 _ (so that w=
e may use it to encapsulate state) and secondly, that it is a model for the=
exponential from linear logic (specifically, it is the cofree commutative =
comonoid over A). I will investigate the underlying reasons why the s=
ame object carries both structures by using the notion of a sequoidal categ=
ory, which generalizes and formalizes the sequoid operator from games, and =
discussing what extra conditions we need to place on it in order to guarant=
ee that the final coalgebra for A =E2=8A=98 _ has the same =
carrier as the cofree commutative comonoid over A. **

**I will give two different situations in which we can make this c=
onclusion. The first is based upon the Melli=C3=A8s-Tabareau-Tas=
son formula for the cofree commutative comonoid in the situation where it c=
an be constructed as a sequential limit of symmetrized tensor powers. =
;The second approach adds the extra axiom that a certain isomorphism from !=
(A =C3=97 B) to !A =E2=8A=97 !B is an isomorphism. This sec=
ond condition always holds in the case that !A is a bifree algebra for =
;A =E2=8A=98 _, but in general it is necessary to impose it, as we est=
ablish by giving an example of a sequoidally decomposable category of games=
in which plays will be allowed to have transfinite length. In this categor=
y, the final coalgebra for the functor A =E2=8A=98 _ is not the cofree comm=
utative comonoid over A: we illustrate this by explicitly contrasting the f=
inal sequence for the functor A =E2=8A=98 _ with the chain of symmetric ten=
sor powers used in the construction by Melli=C3=A9s, Tabareau and Tasson.**

**23 May**

**John Power (Univer=
sity of Bath)**

** A few weeks ago, I gave a seminar on joint work with Richard Garner tha=
t was based upon categories enriched in bicategories. However, I only outli=
ned a definition and only briefly mentioned the context in which they arise=
. So I plan to give an expository talk outlining a few of the one-dimension=
al generalisations of the notion of category that have been studied over th=
e past sixty years, with an idea of how they arose and how they relate to e=
ach other.**

** **

**16 May**

**Alessio Guglielmi =
(University of Bath)Sabbatical Report**In=
the past year we have obtained several results in deep inference, helped b=
y a productive sabbatical for me. In my opinion, it is time to make an effo=
rt and push deep inference into the mainstream.

**In fact, I just found out =
that, contrary to what I have been thinking so far, deep inference has dram=
atic, positive consequences on the complexity of proofs above propositional=
logic. Another reason is that we have now a theory of normalisation that i=
s more powerful and is conceptually clearer than the traditional one.**

**I will give a high-level p=
resentation of the main results of the past year, which are: 1) subatomic l=
ogic and a common structure behind normalisation procedures; 2) elimination=
of cycles and its impact on substitution theory; 3) a generalised understa=
nding of quantification and its impact on the complexity of proofs.<=
/strong>**

**There are opportunities fo=
r several projects that extend or apply those results, in particular on cyc=
lic proofs, process algebras, the epsilon calculus, the Curry-Howard isomor=
phism (on which I recently changed my mind a bit), and more. It would be he=
lpful for me to get feedback on what the best strategy for future grant app=
lications could be.**

**I have been told by many e=
xperienced colleagues that what is needed now, in order to make deep infere=
nce popular, is a textbook. I am convinced that this is necessary and I bel=
ieve that the best way is to found the new theory starting from the notion =
of atomic flow. I will tell you what I think the atomic flows can and shoul=
d do in terms of foundations, but I need your help to approach them from th=
e categorical point of view. (A categorical understanding of atomic flows i=
s necessary because they basically are string diagrams, which are seemingly=
becoming the foundation for quantum theories, which in turn might benefit =
from the compression and computation properties of deep inference.)<=
/strong>**

**2 May**

**John Power (University of Bath)**

** **

**28 March**

**John Power (University of Bath)**

While maintaining that unity, we further refine lax semantics t= o give finitary models of logic progams with existential variables, and to = develop a precise semantic relationship between variables in logic programm= ing and worlds in local state.

** **

**7 March**

**Nicolai Vorobjov (University of Bath) **=

**Schanuel's conjecture is t=
he central, yet unsettled, proposition in transcendental number theory. Mos=
t of the known results (like famous Lindemann-Weierstrass theorem) and othe=
r conjectures in this theory follow from Schanuel. The conjecture turned ou=
t to be useful in model theory/analytic geometry, for example Macintyre and=
Wilkie proved Tarski's conjecture on decidability of the theory of the rea=
ls with exponentiation, assuming Schanuel. Recently I studied, with C. Rien=
er, the structure of irreducible components of real exponential sets, using=
Schanuel. In this talk I will remind the basics of transcentental numbers,=
formulate the conjecture and some of it's consequences.**

**28 February**

**John Power (University of Bath)Clubs, enrichment and=
weak n categories: a progress report**

**In the early 1960's, Jean Benabou proposed the notion of bicateg=
ory: a bicategory bears the same relationship to a 2-category as a monoidal=
category bears to a strict monoidal category, a monoidal category being a =
one-object bicategory and a strict monoidal category being a one-object 2-c=
ategory.**

**It is not difficult to generalise the notion of 2-category to on=
e of n-category for arbitrary n, but generalising the notion of bicategory =
has been a focus of research in both category theory and algebraic topology=
since the late 1980's, and it remains so now. Here, I report on =
progress that Soichiro Fujii, Thomas Cottrell and I have made over the=
past few months, as we have gradually come to understand and, to some exte=
nt, reorganise the approach taken by Michael Batanin in Australia and =
Tom Leinster in Scotland. **

**21 February**

**Marco Solieri (University of Bath)**

**Models of efficient implem=
entation and fine semantics of higher order programming languages both need to include a formal acco=
unt of duplication. Once =
deconstructed, duplication can then be:**

*** avoided - as in the stat=
ic normalisation of proof nets given by Girard's geometry of interaction (GoI);* anticipated - as in the linearisation of lamb=
da terms given by Taylor-=
Ehrhard-Regnier expansion;=
* postponed - as in the optimal implementation of the lambda calculus =
given by Lamping's sharing gra=
phs (SG).**

**How the GoI and the Taylor=
expansion are related? Is the optimal implementation efficient? In this talk I will survey two of t=
he contributions I obtain=
ed in my doctoral investigations, and sketch some the directions of my current or prospective inte=
rest.**

**I will first introduce the=
geometry of resource interaction, a GoI for the resource lambda calculus, that is the linear and no=
n-deterministic variation=
of the ordinary one being the domain of Taylor expansion. The =
algebraic structure which implements =
computation on paths within a term/proof correspond essentially to the multiplicative portion of the=
latter, enriched with a =
superposition operator. An expanded version of Girard's execution formula can then be easily formula=
ted and shown to be invar=
iant under reduction for ground-typed closed terms.**

**Secondly, I will recall th=
at the only general (i.e. not empirical) result about the complexity of SG is restricted to two vari=
ants of linear logic proo=
f-nets, ELL and LLL, which characterise two timecomplexity classes, respectively elementary and polyn=
omial. In these cases, Ba=
illot and Dal Lago have shown exploiting a GoI-like approach that the complexity of SG remains in su=
ch complexity classes. In the same setting, and together with Guerrini, I obtained a direct cost&nbs=
p;comparison between SG and th=
e proof net reduction by purely syntactical means. A simulation between the two reductions allows to=
establish that a stronge=
r bound: a quadratic function.**

** **

**7 February**

**Noam Zeilberger (University of Birmingham)A Categorical Perspective on Type Refinement Sy=
stems**

**A "type refinement system"=
is a type system built on top of a typed programming language, as an extra layer of typing. Type re=
finement systems in this =
sense have become increasingly popular, as a lightweight mechanism for improving the correctness of =
programs. In the ta=
lk, I will give an introduction to a categorical perspective on type refinement systems that I have =
been developing in collaboration with Paul-Andr=C3=A9 Melli=C3=A8s, based on the simple idea of mode=
lling a type refinement s=
ystem as an "erasure" functor from a category of typing derivations to a category of terms. So=
me questions one can consider from this perspective include:**

*** What does it mean for a =
program to have more than one type? What does it mean for a typing judgment to have more than one de=
rivation?**

*** How should we understand=
the so-called "subsumption rule"?**

*** If functors are type ref=
inement systems, what does it mean for a functor to be a Grothendieck (bi)fibration?**=

**A particular class of type=
refinement systems that are especially natural from this perspective are ones coming from a strict =
monoidal closed functor t=
hat is simultaneously a bifibration. I will give some examples illustrating how such type refinement=
systems can be used to g=
ive an axiomatic account of some phenomena from the semantics of separation logic and lambda calculu=
s.**

**24 January**

**Koko Muroya (University of Birmingham)Dynamic Geometry of Interaction machine: call-by-ne=
ed graph rewriter**

**Girard's Geometry of=
Interaction (GoI), that is semantics of Linear Logic pro=
ofs, has been applied to program semantics in mainly two =
styles. One style yields graph rewriting systems for the =
lambda-calculus in which GoI gives an invariant of rewrit=
ing. The other style produces abstract machines that pass=
a token on a fixed graph along a path indicated by GoI.<=
/span> These styles of GoI in program semantics handle duplicati=
on of computation differently with linear logic as a back=
end, and consequently can be efficient in different ways=
.The graph-rewriting GoI achieves time efficiency by copyi=
ng subgraphs, whereas the token-passing GoI is space effi=
cient by repeating moves of a token in a fixed (sub)graph=
. Aiming at exploring this spectrum of space and time eff=
iciency, we introduce an abstract machine called Dynamic =
GoI Machine (DGoIM). It combines graph rewriting with tok=
en passing using a history of token passing.**

** **

__2016 __

**19 December**

**Thomas Strum (CNRS=
, France and MPI for Informatics, Germany)Beautiful Decision Meth=
ods and Adventurous Heuristics for Solving Problems over the Reals&n=
bsp;**

**Effective quantifier elimi=
nation procedures for first-order theories provide a powerful tool for generically solving a wide ra=
nge of problems based on logical specifications. In contrast to general first-order provers, quantif=
ier elimination procedure=
s are based on a fixed set of admissible logical symbols with an implicitly fixed semantics. This ad=
mits the use of subalgorithms from symbolic computation. We are going to start with traditional quan=
tifier elimination applie=
d to verification and simple problems from the life sciences. <=
span style=3D"color: rgb(33,33,33);">Beyond quantifier elimination we are g=
oing to discuss recent results on an incomplete decision procedure for the existential fragment of t=
he reals, which has been =
successfully applied to the analysis of reaction systems in chemistry =
and in the life sciences, whic=
h scales to models currently used in systems biology. We might mention our open-source computer logi=
c software Redlog, where =
our methods are implemented (www.redlog.eu).**

** **

**29 November**

**James Brotherston ( University College London)**

Biabduction (and Related Pr= oblems) in Array Separation Logic

**I describe array separatio=
n logic (ASL), a variant of separation logic in which the data structures a=
re either pointers or arrays. This logic can be used, e.g., to give memory =
safety proofs of imperative array programs. **

**The key to automatically i=
nferring specifications is the so-called " biabduction" problem, gi=
ven formulas A and B, find formulas X and Y such that**

**A * X |=3D B * Y**

**( and such that A * X i=
s also satisfiable), where * is the well-known "separating conjunction=
" of separation logic. We give an NP decision procedure for this prob=
lem that produces solutions of reasonable quality, and we also show that th=
e problem of finding a consistent solution is NP-hard. **

**Along the way, we study sa=
tisfiability and entailment in our logic, giving decision procedures and co=
mplexity bounds for both problems. **

**This is joint work with Ni=
kos Gorogiannis ( Middlesex) and Max Kanovich (UCL). =
A paper describing the work is available at https:/=
/arxiv.org/abs/1607.01993 .<=
/span>**

**22 November**

**Thomas Cottrell (University of Bath)**

**Operads are tools for defi=
ning algebraic structures in terms of the operations they have. In this tal=
k, I will describe the classical case of operads, in which each operation h=
as a natural number of inputs, called its arity. I will then explain how to=
generalise this definition to allow for operads with more complex shapes o=
f inputs. Finally, I will show how these generalised operads can be used to=
define weak n-categories, a very general type of higher-dimensional catego=
ry.**

**15 November**

**Soichiro Fujii** **(The University of =
Tokyo)Generalized Global States**

**From the outset, the globa=
l state has been among the leading examples in the algebraic approach to co=
mputational effects. Indeed, the approach itself started from the recogniti=
on that the global state admits a computationally natural presentation in t=
erms of operations and equations.**

**In this talk, I attempt to=
shed new light on the global states by introducing a new class of computat=
ional effects which I tentatively call `generalized global states'. First, =
I explain that the now standard presentation of the global state monad on S=
et (in terms of the update and lookup operations) is a particular instance =
of a much more general phenomenon, whose first appearance essentially dates=
back to Lawvere=E2=80=99s thesis. Second, I present a unified operational =
semantics for generalized global states and state a relationship to Plotkin=
and Power's operational semantics based on effect values.**<=
/p>

**1 November**

**Mart=C3=ADn Escard=C3=B3 (University of Birmingham)C=
ontinuity in type theory**

**The formulation in Martin-Loef type theory of a Brouwerian =
continuity principle, saying that all functions (N->N)->N are co=
ntinuous, via the so-called Curry-Howard interpretation of logic, turn=
s out to be inconsistent. It becomes consistent under the univalent in=
terpretation of logic, which is similar to that of topos logic. In par=
ticular, the notion of existence is interpreted as something strictly weake=
r than that Martin-Loef's Sigma type, but stronger than its classical =
manifestation as the negation of a universal quantifier. In fact, the =
original paper by Howard already points out that there are two natural=
constructive notions of existence (a weak and a strong one).**

**25 October**

**Pedro Henrique Carrasqueira (CLE, University of Campinas=
, Brazil)Some introductory remarks to paraconsistency and logics of for=
mal inconsistency **

**A logic is paraconsistent if inconsistencies do not imply trivia=
lity in it. Paraconsistent logics are thus suited for reasoning in the pres=
ence of ineliminable inconsistencies, and they produce non-trivia=
l but inconsistent theories. There are two main philosophical traditions of=
studies of inconsistency and paraconsistent logic. One of them advocates f=
or the position known as dialetheism: that some contradiction=
s are true, or, equivalently (given classical negation), that some proposit=
ions are both true and false. There is, however, another, somewhat earlier =
tradition, which takes a very different approach to the matter of inconsist=
ency. This tradition assumes, instead, paraconsistency to be a common trait=
of logics that are in some sense appropriate for situations of imperfect r=
ationality or imperfect information. In particular, their research foc=
uses on logics in which the presence of disagreement or misinformation can =
be expressed by a formal language itself. Collectively, the various logics =
developed by this tradition and having such a property are known as logics of formal inconsistency.&n=
bsp;In my talk I shall briefly discuss the main differences tha=
t keep apart these two traditions of paraconsistency, with special attentio=
n to the different theoretical and practical problems they aim to solve. Th=
en I shall focus on logics of formal inconsistency, taking the logic called=
mbC as my main example of the kind of behavior such log=
ics exhibit. I shall end with some remarks on the ongoing research in this =
tradition of paraconsistency, as well as on its possible further developmen=
ts.**

** **

**4 October**

**David Sherratt (University of Bath) Towards an atomic abstract machine**

**The atomic lambda-calculus is known for its efficiency when eval=
uating terms; it is naturally fully lazy. Abstract machines are used to adm=
inister evaluation strategies. In this talk, I will discuss the idea of bui=
lding an atomic abstract machine, implementing the evaluation strategy for =
the atomic lambda-calculus, with the intent of developing a fully lazy abst=
ract machine and proving it to be effective. **

**Alessio Santamaria (University of Bath)Looking for a=
categorical notion of substitution of atomic flows**

**In this talk I present the work I have done in my first year: tryi=
ng to give a categorical understanding of atomic flows in order to study th=
eir algebra - in the technical sense of the term, that is the operations we=
can do with them. Apart from plugging together and juxtaposing two flows, =
Guglielmi et al. proposed in an unpublished manuscript a notion of sub=
stitution of a flow inside a connected component of another, an operation w=
hich would generalise the usual notion of substitution of a formula inside =
the occurrences of an atom in another formula to that of substitution of a =
derivation inside the occurrences of an atom in another derivation. Categor=
ically speaking, it seems that their idea can be formalised in terms of hor=
izontal composition of families of morphisms, with which we interpret atomi=
c flows. I will show how we generalised the well known definition of h=
orizontal composition of natural transformations for a larger class of fami=
lies of morphisms, namely extranatural transformations, in a mean=
ingful way and what we have in mind to do for families of morphisms wh=
ich are obtained by composing natural and extranatural transformations=
, but themselves are neither of them.**

**1****2 May**

**Giulio Manzonetto (Universit=C3=A9 Paris XIII) New Results on Morris's Observational Theory =
--- The Benefits of Separat=
ing the Inseparable**

**We study the theory of contextua=
l equivalence in the untyped lambda-calculus, generated by taki=
ng the normal forms as observables. Introduced by Morris in 1968, this=
is the original extensional lambda theory H+ of observational equival=
ence. On the syntactic side, we show that this lambda-theory validates=
the omega-rule, thus settling a long-standing open problem. On the se=
mantic side, we provide sufficient and necessary conditions for relati=
onal graph models to be fully abstract for H+. We show that a relation=
al graph model captures Morris's observational pre-order exactly when =
it is extensional and lambda-K=C3=B6nig. Intuitively, a model is lambd=
a-K=C3=B6nig when every lambda-definable tree has an infinite path whi=
ch is witnessed by some element of the model.**

**27 April**

**Pino Rosolini (University of Genoa)**

**We describe a connection between=
frames and algebras for the double exponential monad on the Sierpinski spa=
ce. Instrumental for the presentation is Dana Scott's category Equ of equil=
ogical spaces. We present a subcategory of Equ, closed under the double exp=
onential monad, on which the category of algebras is equivalent to that of =
frames (and frame homomorphisms). I hope to connect this with Taylor's work=
on Abstract Stone Duality.**

**This is joint work with Giulia F=
rosoni and Alessio Santamaria.**

**20 April**

**Jamie Vicary (University of Oxford)**

**Linear logic is a fundamental wa=
y to reason about resources that cannot be duplicated or deleted. In this t=
alk, I will present a new approach to the proof theory of linear logic, in =
which proofs are represented as surfaces embedded in 3-dimensional space. P=
roof equivalence then has a simple definition: two proofs are logically equ=
ivalent just when their surfaces are geometrically equivalent. The technica=
l basis for the work comes from higher category theory, and I will give a s=
imple and accessible introduction to this.**

**19 April**

**Paul Harrenstein (University of Oxford)**

Expressiveness and Nash Equilibrium in Iterated B= oolean Games

** **We introduce and investigate a novel noti=
on of expressiveness for temporal logics that is based on game theoretic pr=
operties of multi-agent systems. We focus on iterated Boolean games, where =
each player has a goal, represented using (a fragment of) Linear Temporal L=
ogic (LTL). This goal captures the player's preferences: the models of the =
goal represent system behaviours that would satisfy the player. Moreover ea=
ch player is assumed to act strategically, taking into account the goals of=
the other players, in order to bring about computations satisfying their g=
oal. In this setting, we apply the standard game-theoretic concept of Nash =
equilibria: the Nash equilibria of an iterated Boolean game can be understo=
od as a (possibly empty) set of computations, each computation representing=
one way the system could evolve if players chose strategies in Nash equili=
brium. Such an equilibrium set of computations can be understood as express=
ing a temporal property=E2=80=94which may or may not be expressible within =
a particular LTL fragment. The new notion of expressiveness that we study i=
s then as follows: what LTL properties are characterised by the Nash equili=
bria of games in which agent goals are expressed in fragments of LTL? We fo=
rmally define and investigate this notion of expressiveness and some relate=
d issues, for a range of LTL fragments.

** **

**12 April**

**Harry Gunn (University of Bath, Masters Student) Nature-based Cryptography**

**This is a review of several papers by G. Grigoriev and V. Shpilr=
ain on a novel approach to public key cryptography. These authors wri=
te: **

**"We use various laws of classical physics to offer =
several solutions of Yao=E2=80=99s millionaires=E2=80=99 problem witho=
ut using any one-way functions. We also describe several informational=
ly secure public key encryption protocols, i.e., protocols secure agai=
nst passive computationally unbounded adversary. This introduces a new=
paradigm of decoy-based cryptography, as opposed to =E2=80=9Ctraditio=
nal=E2=80=9D complexity-based cryptography. In particular, our protoco=
ls do not employ any one-way functions.=E2=80=9D**

**5 April**

**Sam Staton (University of Oxford)**

**I'll talk about the semantics of=
probabilistic programming languages. This is an old subject, but recently =
probabilistic programming has attracted a lot of interest as a method =
of statistical modelling, through languages like Anglican and Church. These=
raise some new problems, such as how to combine continuous distributi=
ons with higher types. I'll describe our work on operational semantics and&=
nbsp;denotational semantics (based on sheaves and measurable spaces). =
**

**15 March**

**John Power (University of Bath) **

Category theoretic semantics for theorem proving in logic pr= ogramming: embracing the laxness

**(joint with Ekaterina Komendantskaya)**

**A propositional logic program P may be identified w=
ith a P _{f}P_{f}-coalgebra on the set of atomic proposition=
s in the program. The corresponding C(P_{f}P_{f})-coalgebra=
, where C(P_{f}P_{f}) is the cofree comonad on P_{f=
}P_{f}_{ }describes derivations by resolution. Us=
ing lax semantics, that correspondence may be extended to a class of first-=
order logic programs without existential variables. The resulting extension=
captures proofs by term-matching resolution in logic programming. Refining=
the lax approach, we further extend it to arbitrary logic programs.**

** **

**8 March**

**John Gowers (University of Bath)**

**I shall present a modification of the Abramsky-Jagadeesan games =
model to allow sequences of moves indexed by transfinite ordinals. Th=
e motivation for this construction is work arising from work by Laird and C=
hurchill in [1,2] concerning the sequoid operator. In [2], the author=
s construct an exponential in the category of games that is a cofree commut=
ative comonoid for the 'tensor on the left' functor and a final coalgebra f=
or the 'sequoid on the left' functor. In the category of finite games=
and strategies, this exponential can be constructed from the sequoid funct=
or as the limit of a diagram indexed by the ordinal w. If we try to e=
xtend this result to the 'sequoidal categories' introduced in [1], then we =
find that this construction does not always produce a final coalgebra, but =
that for natural categories of games a similar construction using a higher =
ordinal will work. If the lengths of plays in an ordinal game can be =
bounded by a limit ordinal k then we may construct the final coalgebra for =
the sequoid using a suitable diagram indexed by k. Conversely, if a g=
ame contains plays greater than an ordinal k then the limit of the natural =
diagram indexed by k does not have the natural structure of a coalgebra.&nb=
sp;**

**There is a sizeable body of research in the field o=
f games with plays indexed by transfinite ordinals (sometimes called 'long =
games'). In [3], Itay Neeman presents results concerning whether or n=
ot such games are determined. More recently, Laird has applied a simi=
lar model to the study of unbounded determinism in [4]. The construct=
ion given in this talk is a straightforward extension of the games model ou=
tlined in [1,5]. A nice feature of the construction is that it includ=
es as special cases both the 'games with winning condition on infinite play=
s', given in [5], and the pure finite games introduced by Blatt in [6].&nbs=
p;**

**After shifting focus from finite to infinite ordina=
ls, it becomes convenient to treat plays (ordinal sequences of moves), rath=
er than moves, as primitive, and one possible formulation is to define a ga=
me to be a sheaf of sets on some given ordinal k, where the ordinal b < =
k is sent to the set of legal plays of length b. In contrast to the A=
bramsky-Jagadeesan model, in which moves are designated as Player-moves or =
Opponent-moves, we have a function that designates plays as Player-plays or=
Opponent-plays. If a play is indexed by a limit ordinal, then it has=
no last move, so this distinction is important. For example, in the =
case of games played over the ordinal w + 1, we are free to specify whether=
a play of length w should belong to Player or to Opponent, and this corres=
ponds exactly to choosing a set of infinite plays that are Player-winning, =
as in [5]. **

**I shall outline the motivation and construction for=
games played over transfinite ordinals, and shall discuss briefly some ten=
tative questions about links to ordinals occurring elsewhere in the theory =
- in particular, game-value ordinals for winning positions and consistency-=
strength ordinals in proof theory.**

**[1]: Martin Churchill, James Laird and Guy McCusker=
. Imperative programs as proofs via game semantics. LICS 2011: =
65-74, June 2011**

**[2]: James Laird. A Categorical Semantics of Higher Order =
Store, CTCS 2002. Proceedings of CTCS '02, Elsevier, 2002**

**[3]: Itay Neeman. The Determinacy of Long Games. De =
Gruyter Series in Logic and its Applications, 1972**

**[4]: James Laird. Sequential Algorithms for Unbounded Nond=
eterminism. MFPS XXXI: 271-287, 2015**

**[5]: Samson Abramsky, Radha Jagadeesan. Games and full com=
pleteness for multiplicative linear logic. Journal of Symbolic Logic =
59 (02): 543-574, 1994**

**[6]: A. Blass. A game semantics for linear logic. An=
nals of Pure and Applied Logic, 56(1-3): 183 - 220, 1992**

**1 March**

**Willem Heijltjes (Univer=
sity of Bath)**

**In this talk I will give an overview of some recent and some ver=
y recent developments in linear logic proof nets.**

__2015__

**8 December**

**Giuseppe Primiero (Middlesex University)**

**Applications in computational domains complement verified knowle=
dge with information sharing processes. From a logical viewpoint, formulati=
ng assertion operations in terms of a trust function is challenging, both c=
onceptually and technically. In this talk we overview SecureND, a natural d=
eduction calculus for knowledge derivation under trust. Its design is motiv=
ated by the problem of trust transitivity. We present also its implementati=
on as the Coq protocol SecureNDC, to deal with trusted sources in software =
management systems. We conclude with an overview of current and future exte=
nsions of our language.**

** **

**1 December**

**Andrea Aler Tubella (University of Bath)**

**Through subatomic logic we are able to present suff=
icient conditions for a proof system to enjoy cut-elimination. In this=
talk I will present subatomic logic, how it enables us to present proof sy=
stems that have single (linear) rule scheme and a recent result: we ca=
n generalise the splitting procedure for cut-elimination to any proof syste=
m whose rules and connectives have certain properties.**

** **

**17 & 24 November**

**John Power (University of Bath) Lawvere Theories**

**I plan to give two talks about Lawvere theorie=
s. These are not for experts but rather to give the details. Lawvere introd=
uced the notion in his PhD thesis in 1963, providing not only a category th=
eoretic account of universal algebra but one that is also presentation-inde=
pendent. Remarkably, his definition was embraced, albeit with a caveat and =
in different terms, by universal algebraists but not by category theorists.=
The latter, from 1966, generally preferred to model universal algebra owin=
g to a little more generality but at a very considerable cost. Computer sci=
entists were then influenced to adopt monads, but much could and has been g=
ained by recasting some of the latter's concerns in terms of Lawvere theori=
es. Ultimately, I think Lawvere theories are a superior approach, but benef=
it very much from the relationship with monads, and I duly plan to explain =
it.**

** **

**27 October**

** Guillaume Munch-Maccagnoni (University of Cambridge) Polarised realizability structures, models, and depolaris=
ation**

**Polarisation describes the presence of an evaluation order, and =
is characterised denotationally by a non-associativity of compositions=
. We recently proposed a polarised, Curry-style approach to the =CE=BB=
-calculus with extensional sums, in correspondence with polarised intu=
itionistic logic. We suggested that associativity of composition in th=
is context should not be seen as a syntactic axiom, but as an emergent=
property akin to termination. Traditionally, issues with sums in deno=
tational semantics have rather been considered to be with extensionali=
ty than with the associativity. This will be explained in an introduct=
ory fashion in a first part.**

**In a second part, I will more formally relate the termination in=
the =CE=BB-calculus with sums to depolarisation, i.e. associativity o=
f composition, or more familiarly the fact that the order of evaluatio=
n does not matter. First, a general setting of polarised realizability=
structures for polarised calculi with or without control operators is=
developed. Then, a general technique to build observational models fr=
om these structures is explained. Finally, under broad conditions, the=
observational models that the non-associative syntactic structure giv=
es rise to satisfy the associativity of composition (and are therefore=
cartesian closed categories with binary co-products). I will sketch a=
n analogy between intuitionistic depolarisation and parametricity.**

** **

**20 October**

** Matthijs V=C3=A1k=C3=A1r (University of Oxford) Game Semantics for Dependent Types**

**Game semantics can act as a unifying semantic framework, providi=
ng compelling models for a strikingly wide range of programming languages, =
type theories and logics. A notable exception has been dependent type theor=
y, which had so far defied a game theoretic description. We present a propo=
sal to fill this gap in the form of a new categorical model of dependent ty=
pe theory, based on a category of games and history-free winning strategies=
. We model dependent type theory with 1-, Sigma-, Pi- and intensional Id-ty=
pes as well as finite inductive type families (which act as ground types, l=
ike calendars). We discuss the place of the Id-types in the intensionality =
spectrum as well as the strong completeness properties the model satisfies.=
**

**Most of the talk should be understandable without prior knowledg=
e of game semantics and dependent type theory.**

** **

**15 October**

**Ugo dal Lago (Universit=C3=A1 di Bologna)**~~Higher-Order Probabilistic Computation: Calculi, Observational Equiva=
lence, and Implicit Complexity~~

**Probabilistic models are more and more pervasive in computer sci=
ence, and randomized algorithms are the ones offering the best performances=
in many domains. Higher-order probabilistic computation =E2=80=93 in which=
a probabilistic function may be passed as a parameter and returned as a re=
sult =E2=80=93 is on the other hand a relatively underdeveloped field, whic=
h is however receiving more and more attention. We give a survey of what is=
known about probabilistic lambda-calculi, later focusing on some of our re=
cent results on implicit complexity and on inductive and coinductive techni=
ques for program equivalence. Finally, we hint at how all this could be use=
ful when structuring proofs of security for cryptographic primitives, but a=
lso when expressing probabilistic models in the context of machine learning=
.**

** **

**10 June**

** Willem Heijltjes (University of Bath)**

**This is joint work with Dominic Hughes. We investigate efficient=
algorithms for the additive fragment of linear logic. This logic is an int=
ernal language for categories with finite sums and products, and describes =
concurrent two-player games of finite choice. In the context of session typ=
es, typing disciplines for communication along channels, the logic describe=
s the communication of finite choice along a single channel.**

**We give a simple linear time correctness criterion for unit-free=
propositional additive proof nets via a natural construction on Petri nets=
. This is an essential ingredient to linear time complexity of the combinat=
orial proofs for classical logic by Dominic Hughes.**

**For full propositional additive linear logic, including the unit=
s, we give a proof search algorithm that is linear-time in the product of t=
he source and target formula, and an algorithm for proof net correctness th=
at is of the same time complexity. We prove that proof search in first-orde=
r additive linear logic is NP-complete.**

** **

**2 June**

** Anupam Das (ENS Lyon)****A complete ax=
iomatisation of MSOL on infinite trees.**

**We show that an adaptation of Peano's axioms for second-order ar=
ithmetic to the language of monadic second-order logic (MSOL) completely ax=
iomatises the associated theory (SkS) over infinite trees. This continues a=
line of work begun by B=C3=BCchi and Siefkes with axiomatisations of MSOL =
over various classes of linear orders. Our proof formalises, in the ax=
iomatisation, a translation of MSO formulas to alternating parity tree auto=
mata. The main ingredient is the formalised proof of positional determinacy=
for the corresponding parity games which, as usual, allows us to complemen=
t automata and to deal with the negation of MSO formulas. The Comprehension=
Scheme of MSOL is used to obtain uniform winning strategies, whereas most =
usual proofs of positional determinacy rely on instances of the Axiom of Ch=
oice or transfinite induction. (Consequently we obtain an alternative decis=
ion procedure for MSOL over infinite trees, via proof search, that remains =
entirely internal to the language.)**

**This talk is based on joint work with Colin Riba that will be pr=
esented at LICS '15.**

** **

**12 May**

** Georg Struth (University of Sheffield)**

**Pomsets form a standard model of true concurrency. In this lectu=
re I present a completeness result for a class of pomset languages, which g=
eneralises the regular languages to the realm of concurrency. More precisel=
y I show that the congruence on series-parallel rational pomset expressions=
generated by series-parallel rational pomset language identity is axiomati=
sed by the axioms of Kleene algebra plus those of commutative Kleene algebr=
a. A decision procedure is extracted from this proof. On the way to this re=
sult, series-parallel rational pomset languages are proved to be closed und=
er the operations of co-Heyting algebras and homomorphisms. These results f=
orm a significant step towards a decision procedure for the equational theo=
ry of concurrent Kleene algebras, which have recently been proposed for con=
currency verification (joint work with Michael Laurence).**

** **

**5 May**

**James Brotherston (University College London) Parametric completeness for separation theories (via hybrid logic=
).**

**In this talk, we consider the logical gap between the following =
two concepts:**

**(1) provability in a propositional axiomatisation of separation =
logic, which is usually given by the bunched logic BBI; and**

**(2) validity in an intended class of models of separation logic,=
as commonly considered in its program verification applications. Such inte=
nded classes are usually specified by a collection of algebraic axioms desc=
ribing specific model properties, which we call a separation theory.**

**Here, we show first that several typical properties of separatio=
n theories are in fact not definable in BBI. Then, we show that these prope=
rties become definable in a natural hybrid extension of BBI, obtained by ad=
ding a theory of naming to BBI in the same way that hybrid logic extends no=
rmal modal logic. Finally, we show how to build an axiomatic proof system f=
or our hybrid logic in such a way that adding any axiom of a certain form y=
ields a sound and complete proof system with respect to the models satisfyi=
ng those axioms. In particular, this yields sound and complete proof system=
s for any separation theory from our considered class (which, to the best o=
f our knowledge, includes all those appearing in the literature).**<=
/p>

**This is joint work with Jules Villard, now at Facebook.**=

** **

**28 April**

**Guilhem Jaber (Queen Mary)****Reasoning=
on Equivalence of Stateful Programs with Operational Game Semantics**

**Contextual equivalence of programs written in a functional langu=
age with references (i.e. local mutable states) is a notoriously hard probl=
em, specially with higher-order references (i.e. references which can store=
functions). In the last twenty years, different techniques have been intro=
duce to that purpose: Kripke Logical Relations, Bisimulations and Algorithm=
ic Game Semantics.**

**In this talk, we will see how to use operational game semantics,=
namely the trace semantics for a language with references introduced by La=
ird, to build a new technique, Kripke Open Bisimulations, to reason on equi=
valence of programs, taking the best of the previous methods. This techniqu=
e is simple enough to be mostly automatized: it becomes possible to model-c=
heck equivalence of programs.**

**If time permits, we will see how to extend this technique to pol=
ymorphism.**

=20

=20
=20

=20
=20

=20
=20

=20
=20

=20