=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 room~~** 6E 2.5 (unless otherwise specified)**** online via Microsoft Teams (https://teams.microsoft.com/l/team/19%3a7398647a739142b49=
9551c59dece2ff6%40thread.tacv2/conversations?groupId=3D2779e154-04d8-464a-9=
035-03cdf22bd135&tenantId=3D377e3d22-4ea1-422d-b0ad-8fcc89406b9e).<=
strong>**

Seminars are open to all.

=20

=20
=20

=20
Organisers: Willem Heijltjes and Giulio Guerrieri an=
d Chris Barrett

Email us to suggest speakers

=20

=20
=20

=20
=20

=20
**Upcoming seminars:**

**1st December **(online via MS Teams)=

**Delia Kesner **(Paris Diderot University)

**The Spirit of Node Replication**

Abstract: We define and investigate a term calculus implementing higher-= order node replication. We use the new calculus to specify two different (w= eak) evaluation strategies: call-by-name and fully lazy call-by-need. We sh= ow that they are observationally equivalent using type theoretical technica= l tools.

=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 univer=
sal algebra are Lawvere theories and finitary (=3D filtered-colimit preserv=
ing) monads on Set. The usual way in which to construct a Lawvere theory fr=
om a finitary monad T is by considering the opposite of the restr=
iction of the Kleisli category Kl(T) to finite sets or equivalently natural=
numbers. Richard Garner recently found a different formulation of thi=
s, 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 mon=
oidal category [Set_f,Set], equivalently the monoidal category [S=
et,Set]f of filtered-colimit preserving functors from Set to Set. =
;
**Logic programming: laxness and saturation**
**(joint with Ekaterina Komendantskaya)**

While maintaining that unity, we further refine lax semantics to give f= initary models of logic progams with existential variables, and to develop = a precise semantic relationship between variables in logic programming and = worlds in local state.
**
****
****
****
****
****
****
****
****
****
****
**

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

__2020__

**23rd November **(online via MS Teams)

**Philip Saville **(University of Edinburgh)

**Type=
theory for cartesian closed bicategories** [join=
t work with Marcelo Fiore]

Cartesian closed bicategories appear in logic, categorical algebra, and = semantics. Roughly speaking, a cartesian closed bicategory is a version of = a cartesian closed category in which the usual beta-eta laws are replaced b= y coherent isomorphisms.

In this talk I will introduce an internal language for cartesian closed = bicategories, and show how the syntax can be extracted in a principled fash= ion from universal-algebraic considerations. The resulting language consist= s of types, terms, and rewrites between terms, together with an explicit su= bstitution operation. By examining the language more closely, we shall see = that it really is --- in a precise sense --- the simply-typed lambda calcul= us `up to isomorphism', and that its rewrites describe beta-eta reductions.= No knowledge of bicategories will be assumed.

**10th November **(online via MS Teams)

**Pawel Sobocinski **(Tallinn University of Technolog=
y)

**Games on graphs: a compositional approach**

Matrices, and more generally linear algebra, play an important role in g=
raph theory. Superficially, adjacency matrices can encode connectivity in a=
graph, but this encoding is often used as a bridge, inviting the transfer =
of concepts and techniques from linear algebra. Categorically speaking, the=
symmetric monoidal category of matrices has an elegant presentation as the=
prop of bimonoids.

With Chantawibul, we explored the addition of "=
caps" and the corresponding natural equations, which turn out to capture th=
e concept of adjacency matrix. Adding generators for vertices, we obtain a =
symmetric monoidal category of "open" graphs. In recent work with Di Lavore=
and Hedges, we extended this to capture multigraphs, and used the resultin=
g category as a "syntax" with which one can define a natural class of games=
as monoidal functors from open graphs to open games. In my talk, I will co=
ncentrate on explaining the basic components of the category of open graphs=
, and sketch the results of the two papers below.

A. Chantawibul an=
d P. Soboci=C5=84ski, "Towards Compositional Graph Theory", In MFPS XXXI, 2=
015

E. Di Lavore, J. Hedges and P. Sobocinski, "Compositional modelling =
of network games", Accepted for CSL 2021. Earlier version available on the =
arXiv (https://arxiv.org/pd=
f/2006.03493.pdf)

**3rd November **(online via MS Teams)=

**Wen Kokke **(University of Edinburgh)

Towards =
Races in Classical Linear Logic

Process calculi based in logic, such as =CF=80DILL and CP, provide a fou=
ndation for deadlock-free concurrent programming, but exclude non-determini=
sm and races. HCP is a reformulation of CP which addresses a fundamental sh=
ortcoming: the fundamental operator for parallel composition from the =CF=
=80-calculus does not correspond to any rule of linear logic, and therefore=
not to any term construct in CP. We introduce HCPND, which extends HCP wit=
h a novel account of non-determinism. Our approach draws on bounded linear =
logic to provide a strongly-typed account of standard process calculus expr=
essions of non-determinism. We show that our extension is expressive enough=
to capture many uses of non-determinism in untyped calculi, such as non-de=
terministic choice, while preserving HCP's meta-theoretic properties, inclu=
ding deadlock freedom*.*

**27th October **(online via MS Teams)

**Mario Alvarez-Picallo **(University of Oxford)

The Difference Lambda-Calculus

Cartesian difference categories are a recent generalisation of Cartesian= differential categories which introduce a notion of =E2=80=9Cinfinitesimal= =E2=80=9D arrows satisfying an analogue of the Kock-Lawvere axiom, with the= axioms of a Cartesian differential category being satisfied only =E2=80=9C= up to an infinitesimal perturbation=E2=80=9D. We present here a simply-type= d calculus in the spirit of the differential =CE=BB-calculus equipped with = syntactic =E2=80=9Cinfinitesimals=E2=80=9D, which provides us with a syntac= tic account of difference categories as well as, surprisingly, a minimalist= ic model for forward-mode Automatic Differentiation.

**6th October **(online via MS Teams)

**Willem Heijltjes **(University of Bath)

D=
ecomposing lambda-calculi with effects

When computational effects are introd=
uced into the lambda-calculus, typically, confluence is lost. Its semantics=
then becomes dependent on a chosen reduction strategy, and since different=
reductions yield different effectful behaviour, it becomes necessary to pr=
ovide means of controlling evaluation within the syntax. The effect is to i=
ntroduce a strong operational component, to the detriment of one of the mai=
n strengths of the (typed) lambda-calculus, which is that is naturally amen=
able to denotational reasoning.

In this talk I will propose a new model of effectful computation: the=
sequential poly-lambda-calculus. Rather than extending the lambda-calculus=
with primitives, it generalizes the existing constructors so that computat=
ional effects as well as the control of evaluation can be decomposed into i=
t. The calculus is confluent, and can be simply typed.

The result is a radically simple model of effe=
ctful computation. The calculus consists of four constructors and a single =
reduction rule (the generalization of beta-reduction), yet it describes mut=
able higher-order store, input and output, random variables, and sequencing=
of commands. It encodes both call-name and call-by-value, as well as previ=
ous approaches to do so, such as Moggi's Computational Metalanguage, Levy's=
call-by-push-value, and Ehrhard and Guerrieri's Bang Calculus. The typed v=
ersion constitutes a new approach to the problem of typing higher-order sto=
re.

**28th July **(online via MS Teams)

**Francesco Gavazzo **(Universit=C3=A0 di Bologna, Ita=
ly)

An Operational Analysis of Algebraic Effects

In this talk, we study the operational theory of a lambda-calculus with = algebraic effects in the spirit of Plotkin and Power. The theory is built o= ver a notion of effectful monadic reduction which extends the standard noti= on of beta-reduction to monadic elements.

We show that for any algebraic effect the notion of reduction thus obtai= ned enjoys a form of finitary standardization, and that if effects are comm= utative, then we also obtain confluence. In presence of arbitrary (algebrai= c) effects, however, both finitary and infinitary reductions exhibit intere= sting computational contents. For this reason, we study asymptotic properti= es of effectful computations and show that even if the reduction is qu= ite liberal, the asymptotic behavior of a term has good computational prope= rties.

This is joint work with Claudia Faggian.

**23rd June **(online via MS Teams)

** Francesco Genco **(Universi=
t=C3=A9 Paris 1, France)

A Parallel Computational = Intepretation of Multiplicative Linear Logic

We present a computational interpretation of multiplicative linear logic= in terms of parallel functional programming. By employing ideas from the d= eduction system on which =CE=BB=CE=BC is based, we define the multiple-conc= lusion natural deduction system NMLL for multiplicative linear logic and we= show that it admits a computational interpretation in terms of communicati= ng parallel processes. The resulting calculus, =CE=BB-par, is a simple exte= nsion of =CE=BB-calculus with parallelism and communication primitives. Aft= er presenting =CE=BB-par, we show some programs which exemplify its express= ive power and we discuss its properties, such as progress, strong normalisa= tion and confluence.

This is joint work with Federico Aschieri, accepted at POPL 2020.

**16th June **(online via MS Teams)

** Gabriele Vanoni **(Universi=
t=C3=A0 di Bologna, Italy)

Geometry of Interaction (GOI) = is a semantic framework describing the dynamics of cut-elimination in the Multiplicative Expone= ntial fragment of Linear Logic (MELL). It has been formulated in many ways, from operator algebras to= traced symmetrical monoidal cate= gories. Remarkably, some of these= formulations, in particular Context Semantics by Gonthier et = al. led to the introduction of compilation techniques (Mackie '95) and abst= ract machines for higher-order functional languages (Danos and Regnier '99)= . However, these machines were always based on a proof-net representation o= f programs, via the so-called Girard translation. We introduce an abstract = machine in the spirit of GOI based directly on the =CE=BB-calculus, without= any explicit use of proof-nets. We prove soundness and adequacy, and we de= rive in our framework an optimization already presented by Danos and Regnie= r. We complete our study with a complexity analysis of those machines.

This is joint work with Beniamino Accattoli and Ugo Dal Lago.

**9th June **(online via MS Teams)

** Sonia Marin **(University C=
ollege London)

A Characterisation of Forwarders as= Linear Logic Proofs

Forwarders are simple processes, within distributed systems of connected= peers, that simply re-send messages. We give a logical account for forward= ing, following a standard proofs-as-processes approach. The main contributi= ons of this paper are two proof systems that characterise (i) non-order pre= serving asynchronous and (ii) synchronous forwarders, respectively. We = ;relate synchronous forwarders to coherence logic, that captures = multiparty compatibility in multiparty session types, and we show that= both systems satisfy deadlock-freedom and compositionality, a property so = far not known to hold for forwarders or other coherence systems.

This is work-in-progress with Marco Carbone and Carsten Sch=C3=BCrmann.<=
strong>

**26th May **(online via MS Teams)

**Ross Horne **(University of Luxembourg)

<=
strong>Logic Beyond Formulae: Generalising the Calculus of Structures =
for Logic on Graphs

Every formula of propositional logic can be written as a graph= with nodes labelled with atomic propositions, where edges joining two= nodes indicate the operator joining the sub-formulae in which th= e respective atoms appear. Those edges can model dependencie= s in logical models of processes. However, restricting to graphs that = formulas generate (co-graphs, series-parallel graphs, etc.) is an arbitrary= restriction from the perspective of modelling processes, since ubiqui= tous structures such as producer-consumer queues form structures that = do not correspond to formulae in this way.

The additional expressive power offered by graphs motivates us in this f= undamental study, where we design a proof system where inference rules= are applied directly to graphs rather than formulae. In designing the= proof system, we assume only that the logic has an involutive ne= gation (which can only be defined by graph complement), and implication is = defined as "not P, or Q", where "or" is the disjoint union of graphs. = The inference rules of the proof system then follow from fundamen= tal principles of logic, most of which are established via cut el= imination, and an assumption that we aim for the minimal and hence most gen= eral system conforming to such principles. Note, applying the same pri= nciples to a logic based on formulae yields multiplicative linear= logic (MLL); and indeed we obtain a conservative extension of MLL to graph= s. Beyond discovering a new system, insight for logic is that (1) = ;deep inference is necessary even for this most basic generalisation o= f logic to graphs; (2) we were forced to generalise the tools of deep infer= ence itself, deepening techniques such as splitting, context reduction, and= rule elimination. Thereby, we discover a proper generalisation of the= calculus of structures, which already generalises the sequent calculu= s, which is fundamental to structural proof theory.

This is joint work with Matteo Acclavio and Lutz Stassburger, to ap= pear in LICS'20.

**19th May **(online via MS Teams)

** Victoria Barrett **(Univers=
ity of Bath)

Towards a normalisation methodology and a topologic= al representation of proofs

In this talk I will discuss the progress made so far in developing a nor= malisation methodology and a representation of proofs. My project will buil= d on Gundersen's atomic flows and Aler Tubella=E2=80=99s subatomic logic. S= ubatomic logic treats atoms as connectives and obtains a linear rule shape = for a wide variety of proof systems. By generalising the rule shape further= we will be able to capture modality and quantification in the open deducti= on formalism and to factor out associativity to obtain good proof semantics= . A good representation will provide induction measures for the normalisati= on of proofs, and provide proof invariants.

I have developed a preliminary proof representation, which tracks the co= nnectives in a subatomic derivation. I will use this to show how a generali= sation of the cut-contraction rewrite rule from atomic flows can be applied= more widely than initially expected, and I will show how the binary subato= mic rule shape could be generalised. In the sense that subatomic logic give= s us a universal rule shape which can be applied to a wide range of logics,= we hope to find universal rewrite rules which will unify the normalisation= of a range of logics.

**12th May **(online via MS Teams)

** Thomas Powell **(University=
of Bath)

Quantitative Tauberian theorems

In this talk I seek to achieve two things. First, I aim to give a very c= oncise introduction to modern applied proof theory, without assuming any pr= ior knowledge of this area. Second, I will present some new reasearch of mi= ne in Tauberian theory, ncuding a proof theoretic study of the celebrated H= ardy-Littlewood Tauberian theorem.

**5th May **(online via MS Teams)

**Davide Barbarossa=
**(Universit=C3=A9 Sorbonne Paris Nord, France and Universit=C3=A0 =
Roma Tre, Italy)**Approximating functional programs: Taylor subsu=
mes Scott, Berry, Kahn and Plotkin.**

In their fundamental pape= r developing the differential =CE=BB-calculus in 2003, T. Ehrhard and L. R= =C3=A9gnier write: "Understanding the relation between the term and its ful= l Taylor expansion might be the starting point of a renewing of the theory = of approximations".

This speculative ambition= is nowadays at hand: using the resource sensitive theory differential =CE= =BB-calculus comes with, we provide "simpler" proofs of crucial results in = =CE=BB-calculus - that are otherwise obtained via Scott=E2=80=99s continuit= y, Berry=E2=80=99s stability or Kahn and Plotkin=E2=80=99s sequentiality th= eory.

This is joint work with G= iulio Manzonetto, accepted at POPL 2020.

**28th April =
**(online via MS Teams)

**Gabriel Scherer <=
/strong>(INRIA Saclay, France)**

Focusing on lambda-calculus= equivalence

In this overview talk we = will show how the logical technique of focusing can be applied to better un= derstand program equivalence in the simply-typed lambda-calculus with datat= ypes (in particular sums and the empty type).

The talk will not assume =
familiarity with focusing, and introduce it in the context of propositional=
intuitionistic logic. We will then present a focused presentation of the (=
normal forms of the) lambda-calculus. If time allow, we will then introduce=
the "saturated" normal forms, a stronger restriction that we used in a pap=
er POPL 2017 (available on http=
s://arxiv.org/abs/1610.01213) to decide equivalence of simply-typed lam=
bda-terms with sums and the empty type.

**21st April **(at 14:00, online via MS Teams)=

**Damiano Mazza** (CNRS-Universit=C3=A9 Paris =
13, France)**Automatic Differentiation in PCF **

Automatic differentiation (AD) is the science of efficiently computing t= he derivative (or gradient, or Jacobian) of functions specified bycomputer = programs. It is a fundamental tool in several fields, most notably ma= chine learning, where it is the key for training deep neural networks. = ; Albeit AD techniques traditionally focus on a restricted class of program= s, namely first-order straight-line programs, the rise of so-called differe= ntiable programming in recent years has called for the need of applying AD = to complex code, containing all sorts of control flow operators and higher-= order combinators. In this talk, I will discuss the extension of AD algorit= hms to PCF, a(n idealized) purely functional programming language. We= will first consider the simply-typed lambda-calculus, showing in particula= r how linear negation is related to reverse mode AD (aka backpropagation), = and then see how the extra features of PCF, namely full recursion and condi= tionals, may be dealt with, stressing the difficulties posed by the latter.=

Joint work with Alo=C3=AFs Brunel (Deepomatic) and Michele Pagani (IRIF,= Universit=C3=A9 de Paris) accepted at POPL 2020.

**14th April **(online via MS Teams)

**Pierre Clairambault** (CNRS-ENS Lyon, France=
)**Fix Your Semantic Cube Using This Simple Trick **

Game semantics usually present execution as a total chronological orderi= ng of observable computational events. They proved to be a powerful tool in= semantics, yielding a great deal of full abstraction results. Its first fe= w achievements were striking, capturing in a single framework combinations = of state and control. This lead to Abramsky's famous "semantic cube" progra= mme: to capture in a single canvas a wide variety of effects. However, past= the original "semantic square" resulting from the combinations of control = and state, developments in game semantics have since then been rather disco= nnected.

The family of game semantics usually known as "concurrent games", origin= ally introduced by Abramsky and Melli=C3=A8s in 1999, has been actively dev= eloped in the past decade or so. In contrast with the total chronological o= rdering of traditional games, concurrent games present (implicitly or expli= citly) the causal constraints between computational events. To that end the= y borrow tools from concurrency theory, and in particular rely on structure= s coming from "true concurrency". They are therefore well suited to the den= otational semantics of concurrent programming languages.

In this talk, I will give an introduction to concurrent games and presen= t some developments that highlight a different property: they are good at l= inking distinct models with each other, in and outside of game semantics. C= oncretely, I will present the first steps to fixing the cube {state, parall= elism, probabilities} -- all its faces are currently broken. First, I will = fix the face {state, parallelism}. For that I will introduce a notion of pa= rallel innocence, exploiting the causal aspect of concurrent games. Time pe= rmitting, I will also fix {state, probabilities}, via probabilistic concurr= ent games and their link with weighted relational semantics. I will close o= n some perspectives on the full cube.

This talk builds on joint work with several people, among whom Simon Cas= tellan, Hugo Paquet and Glynn Winskel.

**31st March **(online via MS Teams)

**Willem Heijltjes** (University of Bath)

<=
strong> Decomposing Probabilistic Lambda-Calculi

A notion of probabilistic lambda-calculus usually comes with a prescribe= d reduction strategy, typically call-by-name or call-by-value, as the calcu= lus is non-confluent and these strategies yield different results. This is = a break with one of the main advantages of lambda-calculus: confluence, whi= ch means results are independent from the choice of strategy.

We present a probabilistic lambda-calculus where the probabilistic opera= tor is decomposed into two syntactic constructs: a generator, which represe= nts a probabilistic event; and a consumer, which acts on the term depending= on a given event. The resulting calculus, the Probabilistic Event Lambda-C= alculus, is confluent, and interprets the call-by-name and call-by-value st= rategies through different interpretations of the probabilistic operator in= to our generator and consumer constructs.

We present two notions of reduction, one via fine-grained local rewrite = steps, and one by generation and consumption of probabilistic events. Simpl= e types for the calculus are essentially standard, and they convey strong n= ormalization. We demonstrate how we can encode call-by-name and call-by-val= ue probabilistic evaluation.

This is joint work with Ugo dal Lago and Giulio Guerrieri, accepted at F= oSSaCS 2020.

**18th February**** **

**Anupam Das **(University of Birmingham)

Some r=
ecent developments in non-wellfounded proof theory

Non-wellfounded proof theory has become a popular alternative to systems= with induction or with infinitely branching rules. The non-wellfounded app= roach to infinitary proof theory retains finitary branching at the cost of = wellfoundedness, naturally requiring some global correctness criterion to p= revent fallacious reasoning. Both wellfounded and non-wellfounded infinitar= y proof theory have the advantage of being amenable to metalogical argument= s for proof analysis (e.g. cut-elimination), but the non-wellfounded approa= ch exhibits a further advantage: there is a natural class of finite proofs,= namely those whose dependency graphs are finite, known as 'circular' or 'c= yclic' proofs.

Non-wellfounded proofs were considered early on in the history of logic,= due to theirassociation with non-standard models of arithemetic (indeed, t= his was one of the moti-vations behind Mints=E2=80=99 continuous cut-elimin= ation). Cyclic proofs themselves seem to first appear in the '90s and =E2= =80=9900s in the study of modal fixed point logics, where regular tableaux = were obtained in a general way thanks to the celebrated Niwinski-Walukiewic= z games. In the '00s Brotherston and Simpson, inspired by that approach, co= nstructed non-wellfounded systems of predicate logic extended by forms of i= nductive definitions. More recently the French school of proof theory has p= ioneered the study of cyclic type systems, motivated by the Curry-Howard co= rrespondence and admitting a more structural proof-theoretic treatment.

This talk aims to give an overarching (and personal) view of the world o= f circular proof theory today. In particular, I will try to promote a class= ical viewpoint of bridging the somewhat disconnected worlds therein by mean= s of correspondences that, in a formal sense, preserve computational conten= t. To this end I will concentrate, as a case study, on the bridge between f= irst-order arithmetic and simply typed recursive programs induced by Goedel= =E2=80=99s functional interpretation.

**28th January**** **(room

**James Laird **(University of Bath)

A Curry-sty=
le Semantics of Interaction: From untyped to second-order lazy lambda=
-mu calculus

We propose a "Curry-style" semantics of programs in which a nomina= l labelled transition system of types, characterizing observable behaviour,= is overlaid on a nominal LTS of untyped computation. This leads to a notio= n of program equivalence as typed bisimulation.

Our semantics reflects the role of types as hiding op= erators, firstly via an axiomatic characterization of "parallel composition= with hiding" which yields a general technique for establishing congruence = results for typed bisimulation, and secondly via an example which captures = the hiding of implementations in abstract data types: a typed bisimulation = for the lazy lambda-mu calculus with (Curry-style) polymorphic typing. This= is built on an abstract machine for CPS evaluation of -terms: we first giv= e a basic typing system for this LTS which characterizes acyclicity of the = environment and local control flow, and then refine this to a = polymorphic typing system which uses equational constraints on instantiated= type variables, inferred from observable interaction, to capture behaviour= at polymorphic and abstract types.

In this informal talk, I will introduce the concept of explainability fo= r Artificial Intelligence and the needs of the field with respect to proof = theory. I will discuss some ideas on how deep inference research could help= in the development of languages to encode explanations through the design = of systems with good complexity/analiticity/proof = search properties that support connectives that can express concepts like s= equentiality, probabilities or causality in a modular way. Thoughts = and discussion about possible research directions are highly encouraged.

__2019__

**11th December ** (Wednesday, at 13:15 in room** 3E 2.4**)

**Andrea Aler Tubella **(=
Umea University, Sweden)

In this informal talk, I will introduce the concept of explainability fo= r Artificial Intelligence and the needs of the field with respect to proof = theory. I will discuss some ideas on how deep inference research could help= in the development of languages to encode explanations through the design = of systems with good complexity/analiticity/proof = search properties that support connectives that can express concepts like s= equentiality, probabilities or causality in a modular way. Thoughts = and discussion about possible research directions are highly encouraged.

**19th November**

**Lutz Strassburger (**Inria, France)

Focusing is a general technique for transforming a sequent proof system =
into one with a syntactic separation of non-deterministic choices without s=
acrificing completeness. This not only improves proof search, but also has =
the representational benefit of distilling sequent proofs into

syntheti=
c normal forms. We show how to apply the focusing technique to nested seque=
nt calculi, a generalization of ordinary sequent calculi to tree-like inste=
ad of list-like structures. We thus improve the reach of focusing to the mo=
st commonly studied modal logics, the logics of the

modal S5 cube. Amon=
g our key contributions is a focused cut-elimination theorem for focused ne=
sted sequents.

**Benjamin Ralph **(Inria, France)

Recent work by Alessio Guglielmi and Andrea Aler Tubella has provided a = unified theory of normalisation for a wide variety of logics, using a subat= omic variant of the deep inference proof methodology. This involves d= istinguishing "cut-like" rules and "contraction-like" rules. The norm= alisation procedure for the former is not dissimilar to the notion of cut e= limination that is foundational to proof theory. However normalising the la= tter, by decomposing the proof into a contractive and non-contractive phase= , is less familiar, as, for many logics, the normal forms obtained are not = expressible in the sequent calculus.

In this talk, I will focus on decomposition for classical propositional =
logic. In the absence of a certain type of cycles in the proof, =
this is straightforward, one can simply "push" the contractions through the=
proof until they are distilled from the other inference rules. Yet, if the=
se cycles are present, one must either remove the cycles first, or take a d=
ifferent approach. In a previous paper, we explored the first option. =
I will describe work taking the other approach, defining a new generalised=
form of contraction, the *merge contraction* and developing it=
s rewriting theory to avert the problem of cycles. Despite originating as a=
solution to a particular problem, I will also argue that these merge contr=
actions are an interesting object of study in their own right, with a natur=
al coinductive definition and many interesting properties.

**14th November **(Thursday, 13:45-15:05, room** 6E 2=
.2**)

**No=
buko Yoshida **and

Game semantics and session types are two formalisations of the same conc= ept: message-passing open programs following certain protocols. Game semant= ics represents protocols as games, and programs as strategies; while sessio= n types specify protocols, and well-typed =CF=80-calculus processes model p= rograms. Giving faithful models of the =CF=80-calculus and giving a precise= description of strategies as a programming language are two difficult prob= lems. In this talk, we show how these two problems can be tackled at the sa= me time by building an accurate game semantics model of the session =CF=80-= calculus.

Our main contribution is to fill a semantic ga= p between the synchrony of the (session) =CF=80-calculus and the asynchrony= of game semantics, by developing an event-structure based game semantics f= or synchronous concurrent computation. This model supports the first truly = concurrent fully abstract (for barbed congruence) interpretation of the syn= chronous (session) =CF=80-calculus. We further strengthen this corresponden= ce, establishing finite definability of asynchronous strategies by the inte= rnal session =CF=80-calculus. As an application of these results, we propos= e a faithful encoding of synchronous strategies into asynchronous strategie= s by call-return protocols, which induces automatically an encoding at the = level of processes. Our results bring session types and game semantics into= the same picture, proposing the session calculus as a programming language= for strategies, and strategies as a very accurate model of the session cal= culus. We implement a prototype which computes the interpretation of sessio= n processes as synchronous strategies.

**5th November**

**Federico Olimpieri **(Aix-Marseille Universit=C3=A9, France)

Intersection types as generalized species: a bicategorical m= odel for pure lambda-calculus

The bicategory of Generalised species is a = generalisation of both the category of sets and relations and Joyal's Speci= es of structures. It can be described as the Kleisly category of a suitable= pseudo-comonad on distributors. In a recent paper, Tsukada, Asada and = ;Ong introduced a denotational semantics via Generalised specie= s with a type-theoretic flavour. Their model is a refinement of t= he classic Gardner-De Carvalho's commutative non-idempotent intersection.&n= bsp; We further generalise their work in two ways. Firstly= , we present a model for pure lambda-calculus, for the algebraic lambda-cal= culus and for the bang-calculus. Secondly, we show how it is possible to pr= esent models that gives rise to more informative intersection type sys= tems (e.g. systems that admits a form of subtyping).

**29th October**

**Matteo Acclavio (Universit=C3=A0 Roma Tr=
e, Italy)**(join=
t work with

Combinatorial proofs for modal logic

Combinatorial proofs are a sound and complete system for classical logic= , which allow to capture the notion of proof equivalence. Combinatorial pro= ofs consists of morphism from a graph equipped with a perfect matching to a= graph representing a formula. In this talk I will present the graphical sy= ntax of combinatorial proofs and show how the formalism can be extended to = obtain a sound and complete proof system for the modal logics of the S4 pla= ne.

This work appeared at Tableaux 2019 (link to the paper).

**Roberto Maieli **(Universit=C3=A0 Roma Tre, Italy)

We investigate the notion of generalized connectives for multiplicative = linear logic. To define such new connectives, we introduce a notion of orth= ogonality for partitions of a finite set and we study the relation between = orthogonality and dual connectives. For such connectives, we give a notion = of decomposability by means of conjunction and disjunction. Finally, we sho= w the existence of a family of non-decomposable connectives which have a si= mple interpretation as superposition of decomposable connectives.

This work will appear at CSL 2020.

**8th October**

**Giulio Guerrieri **(University of Bath)**Factorization and Normalization, Essentially** (joint work with** ****Beniamino Accattoli and Claudia Faggian)**

Lambda-calculi come with no fixed evaluation strategy. Different strateg= ies may then be considered, and it is important that they satisfy some abst= ract rewriting property, such as factorization or normalization theorems. I= n this paper we provide simple proof techniques for these theorems. Our sta= rting point is a revisitation of Takahashi's technique to prove factorizati= on for head reduction. Our technique is both simpler and more powerful, as = it works in cases where Takahashi's does not. We then pair factorization wi= th two other abstract properties, defining essential systems, and show that= normalization follows. Concretely, we apply the technique to four case stu= dies, two classic ones, head and the leftmost-outermost reductions, and two= less classic ones, non-deterministic weak call-by-value and least-level re= ductions.

This work will appear at APLAS 2019.

**30th July (room 1W 2.03)**

** Ugo Dal Lago (Universit=C3=A0 di B=
ologna, Italy)**(joint work with

We introduce a new form of logical relation which, in the s= pirit of metric relations, assigns each pair of pr= ograms a quantity measuring their distance, rather than a boolean valu= e standing for their being equivalent (or not). The novelty of differential= logical relations consists in measuring the distance between terms no= t (necessarily) by a numerical value, but by a mathematical object whi= ch somehow reflects the interactive complexity, i.e. the type, of the = compared terms. We exemplify this concept in the simply-typed lambda-calcul= us, and show a form of soundness theorem. We also see how ordinary log= ical relations and metric relations can be seen as instances of differ= ential logical relations. Finally, we show that differential logical r= elations can be organised in a cartesian closed category, contrarily to met= ric relations, whichare well-knownnotto have such a structure, but only tha= t of a monoidal closed category. We conclude the talk by hinting at other f= orms of differential program semantics, which are being studied as part of = the DIAPASoN research project.

This work appeared at ICALP 2019 (link to the paper).

**-------------------------------=
------------------------------------------------**

**Informal Workshop Micro Structu=
res and Deduction (Micro-SD)**

** **--------------

**Wednesday 29 May (Room 3W 3.7)**

1:15 Adam Lassiter (Bath): Coalescence Proof Search for Cla=
ssical Logic

2:00 Michelangelo Mecozzi (Bath): Expansion Tr=
ee Proofs with Unification

2:45 --- Coffee break ---

&nb=
sp; 3:15 Chris Barrett (Bath): A Subatomic Proof System for Decision =
Trees

4:15 --- End ---**Monday 3 June (Room 8=
W 1.33)**

1:15 Delia Kesner (Paris 7): Principles of Quantitative Typ=
es for Higher-Order Languages

2:15 David Sherratt (Jena): T=
he Spinal Atomic Lambda-Calculus

2:45 --- Coffee break ---<=
br> 3:15 Giulio Guerrieri (Bath): Standardization via Linear Lo=
gic for Call-by-Name, Call-by-Value and Choice Effects

4:00 =
Benjamin Ralph (INRIA Paris): Towards a Combinatorial Proof Theory ** 4:45 --- End ------------------ **

**Adam Lassiter (University of Bath) **

*Coalescence Proof Search for Classical Logic*

Coalescence is a highly efficient proof search method for additive linea= r logic, the logic of categorical sum and product. For a proof of a sequent= over two formulas A and B, it is a linear algorithm on the 2-dimensional p= roduct space |A|x|B| over the subformulas |A| of A and the subformulas |B| = of B. By design, the algorithm has no need for backtracking, and has built-= in sharing (or memoization).

In this talk, I discuss how to adapt this method for classical logic. Th= e starting point is the observation that a classical formula A can be prove= d by n-dimensional coalescence - that is, there is some n such that A can b= e proved by coalescence over the space |A|x|A|x...x|A| (with n copies of |A= |).

Whether this algorithm is efficient depends on the growth of n. In a nai= ve approach, this growth is far worse than expected. I will then discuss so= me natural ways of optimizing the algorithm.

-----

**Michelangelo Mecozzi (Univeristy of Bath)**

*Expansion Tree Proofs with Unification*

Expansion tree proofs are a repre=
sentation of proofs in first-order classical logic that is focused on the w=
itnessing terms to existential quantifiers, factoring out both propositiona=
l proof content (which is decidable) and the bureaucracy of sequent calculu=
s. They are based on Herbrand's theorem, and have a natural game-semantic i=
nterpretation. There is also an interesting connection with learning algori=
thms.

Herbrand's theorem, however, makes no mention of explicit witnesses. In = line with this, Hughes, Heijltjes, and Strassburger have recently given pro= of formalisms for fragments of first-order linear logic that omit witnessin= g terms, and instead reconstruct these by unification.

In this talk, I will apply this idea to expansion tree proofs, yielding =
a variant that omits witnessing terms, and discuss algorithms to reconstruc=
t these.

-----=

**Chris Barrett (University of Bath)**

*A Subatomic Proof System for Decision Trees*

Recently, several proof systems h=
ave been developed in a very principled and regular way according to a meth=
odology called 'subatomic'. The main idea is to consider atoms as non-commu=
tative self-dual connectives representing a superposition of truth values. =
This way, non-linear inference rules, such as contraction and cut, become l=
inear and obey a unique scheme. Normalisation is, therefore, at the same ti=
me, simplified and generalised. The contribution of this talk is that, surp=
risingly, by completing in the most natural way the standard subatomic proo=
f system for propositional classical logic, we obtain a new proof system fo=
r a conservative extension of propositional classical logic and of binary d=
ecision trees. Cut elimination for this system becomes an almost trivial va=
riation of the already known (and also trivial) 'experiment method', which =
is essentially a truth tabling operation that generates canonical analytic =
proofs.

-----

**Delia Kesner (Universit=C3=A9 d=
e Paris, IRIF, CNRS)**

*Principles of Quantitative Types for Higher-Order Languages<=
/em>*

Quantitative techniques are emerging in different areas of computer scie= nce (model checking, logic, automata theory, etc) to face the challenge of = today's resource aware computation.

In this talk we discuss quantitative types, a.k.a. non-idempotent (inter= section/union) types, which provide a natural tool to reason about resource= consumption. Quantitative types are applicable to a wide range of powerful= models of computation, including pure functional programming, pattern matc= hing, control operators and infinitary computations.

We provide a clean theoretical understanding of the use of resources, an= d survey some recent semantical and operational results in the domain.

------

**David Sherratt (University of J=
ena)**

*The Spinal Atomic Lambda-Calculus*

We introduce a variant of Gundersen, Heijltjes, and Parigot's atomi= c lambda-calculus. This typeable calculus with explicit sharing extends the= Curry-Howard interpretation of open deduction already established by = the previous calculus. This expanded interpretation allows us to = follow a duplication strategy stronger than full laziness, in the sens= e that we duplicate less and share more of a term. This new ability is stro= ngly connected to interpreting the scopes of abstractions, which is st= rongly related to the open deduction system in turn. We establish the = good operational behaviour of the language by means of some fundamenta= l properties such as confluence and preservation of strong normalisation.&n= bsp;We finally discuss the possible benefits of this calculus, which may le= ad to some remarkable breakthroughs.

------

**Giulio Guerrieri (University of=
Bath)**

*Standardization via Linear Logic for Call-by-Name, Call-by-V=
alue and Choice Effects*

Linear Logic (LL) has proved powerful in providing insights and tools to= analyze computational and denotational properties of programming languages= . When considering the lambda-calculus, LL provides a common setting where = both call-by-name (CbN) and call-by-value (CbV) evaluation mechanisms can b= e interpreted via Girard's translations. The bang calculus internalizes the= insights coming from LL proof-nets into an untyped lambda-like syntax whic= h subsumes both CbN and CbV. In a different sense, the idea of a system whi= ch subsumes both CbN and CbV had been already advocated and developed by Le= vy, via the Call-By-Push-Value paradigm; and indeed, the bang calculus can = be seen as an untyped version of Levy's one. This approach has been mainly = exploited semantically. Moreover, the Call-by-Push Value paradigm, as well = as related polarized calculi, admits LL-based models featuring non-trivial = computational effects such as non-deterministic or probabilistic computatio= ns.

We show that the bang calculus provides a powerful methodology to study = syntactical properties of CbN and CbV, and their extension to calculi with = a choice effect (such as probabilistic, non-deterministic, or quantum). In = particular, we have a uniform method to study the fundamental syntactical r= esults for CbN and CbV lambda-calculi: confluence, standardization and norm= alization, and their extension to calculi with effects. Our approach allows= us not only to revisit some well-known results, but also to discover new o= nes, namely in studying calculi with effects.

-----

**Benjamin Ralph (Inria Paris Saclay)**

*Towards a Combinatorial Proof Theory*

Combinatorial proofs have been introduced by Hughes to give a ``syntax-f= ree'' presentations for proofs in classical propositional logic. In a nutsh= ell, a classical combinatorial proof consists of two parts: (i) a linear pa= rt, and (ii) a skew fibration. The linear part encodes a proof in multiplic= ative linear logic (MLL), whose conclusion is given represented in a cograp= h, while the skew fibration maps this linear cograph to the cograph of= the conclusion of the whole proof. In deep inference, this skew fibr= ation corresponds exactly to a contraction-weakening derivation. Applying c= ertain restrictions to these two rules leads to substructural logics and su= bstructural proof theory. These proof theoretic restrictions correspond pre= cisely to set-theoretic and graph-theoretic restrictions on the skew fibrat= ion, allowing us to characterise proof systems by their graph homomorphism = class.

------------------------------

**21st May (room 1W 3.107)**

**Cristina Matache (University of Oxford)**(joint work with

A Sound and Complete Logic for Alge= braic Effects

I will talk about definitions of program equivalence, for a language wit= h algebraic effects in the style of Plotkin and Power. Program equivalence = is a long-standing problem in computer science, made more difficult by the = presence of higher-order functions and algebraic effects. In this talk I wi= ll present a logic whose formulas represent properties of effectful program= s. The satisfaction relation of the logic induces a notion of program equiv= alence. Notably, the induced equivalence coincides with contextual equivale= nce (which equates programs with the same observable behaviour) and also wi= th an applicative bisimilarity.

This is joint work with Sam Staton which appeared at FOSSACS 2019. (link to the article)

**16th April**

**Alessio Santamaria (University of Bath)**

Towa= rds a Godement Calculus for Dinatural Transformations

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

- Acyclicity of certain graphs associated to dinatural transformations is= a sufficient and essentially necessary condition for two dinatural transfo= rmations to compose;
- This yields to the definition of a category whose objects are mixed-var= iant functors and morphisms are partially dinatural transformations;
- A new definition of horizontal composition for dinatural transformation= s embodying substitution of functors into transformations and vice-versa, i= ntuitively reflected from the string-diagram point of view by substitution = of graphs into graphs.

This work represents the first, fundamental steps towards a Godement-lik=
e calculus of dinatural transformations as sought=E2=80=94but never achieve=
d=E2=80=94by Kelly in [5], with the intention then to apply it to describe =
coherence problems abstractly [6]. We have not managed to get such a comple=
te calculus yet, but we are =E2=80=9Cwell on our way=E2=80=9D on the path p=
aved by Kelly himself in [5] when he was assessing the simpler case of a ma=
ny-variable __fully covariant__ functorial calculus. What we have not do=
ne yet will be the subject of future work.

[1] Bainbridge, E.S., Freyd, P.J., Scedrov, A. and Scott, P.J., 1990. Fu=
nctorial polymorphism. *Theoretical Computer Science* [Online], 70(1=
), pp.35=E2=80=9364. Available from: https://doi.or=
g/10.1016/0304-3975(90)90151-7.

[2] Girard, J.-Y., Scedrov, A. and Scott, P.J., 1992. Normal Forms and C=
ut-Free Proofs as Natural Transformations. In: N.M. Yiannis, ed. *Logic =
from Computer Science*, [Online]. Mathematical Sciences Research Instit=
ute Publications. Springer, New York, NY, pp.217=E2=80=93241. Available fro=
m: https://doi.org/10.1007/978-1-4612-2822-6_8.

[3] Blute, R., 1993. Linear logic, coherence and dinaturality. *Theor=
etical Computer Science* [Online], 115(1), pp.3=E2=80=9341. Available f=
rom: https://doi.org/10.1016/0304-3975(93)90053-V.

[4] Dubuc, E. and Street, R., 1970. Dinatural transformations. In: S. Ma=
c Lane, H. Applegate, M. Barr, B. Day, E. Dubuc, A.P. Phreilambud, R. Stree=
t, M. Tierney and S. Swierczkowski, eds. *Reports of the Midwest Categor=
y Seminar IV*, [Online]. Lecture 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-variable functorial calculus. I. In: G.M. Ke=
lly, M. Laplaza, G. Lewis and S. Mac Lane, eds. *Coherence in Categories=
*, [Online]. Lecture Notes in Mathematics. Springer, Berlin, Heidelberg=
, pp.66=E2=80=93105. Available from: https://doi.org/10.1007/B=
Fb0059556.

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

**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 introduced t= o capture algebraically the presence of state in history-sensitive strategi= es in game semantics, by imposing a causality relation on the tensor produc= t of games. Coalgebras for the functor A =E2=8A=98 _ - i.e., morphisms= 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 state trans= former encapsulates its explicit state, so that it is shared only between s= uccessive invocations.

When we use this construction to model stateful objects in game semantic= s, we are using two properties of the game !A: firstly, that it is the= final coalgebra for the functor A =E2=8A=98 _ (so that we may us= e it to encapsulate state) and secondly, that it is a model for the exponen= tial from linear logic (specifically, it is the cofree commutative comonoid= over A). I will investigate the underlying reasons why the same obje= ct carries both structures by using the notion of a sequoidal category, whi= ch generalizes and formalizes the sequoid operator from games, and discussi= ng what extra conditions we need to place on it in order to guarantee 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 conclusio= n. The first is based upon the Melli=C3=A8s-Tabareau-Tasson form= ula for the cofree commutative comonoid in the situation where it can be co= nstructed as a sequential limit of symmetrized tensor powers. The sec= ond approach adds the extra axiom that a certain isomorphism from !(A =C3= =97 B) to !A =E2=8A=97 !B is an isomorphism. This second co= ndition 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 establish= by giving an example of a sequoidally decomposable category of games in wh= ich plays will be allowed to have transfinite length. In this category, the= final coalgebra for the functor A =E2=8A=98 _ is not the cofree commutativ= e comonoid over A: we illustrate this by explicitly contrasting the final s= equence for the functor A =E2=8A=98 _ with the chain of symmetric tensor po= wers used in the construction by Melli=C3=A9s, Tabareau and Tasson.

**23 May**

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

A few weeks ago, I ga= ve a seminar on joint work with Richard Garner that was based upon categori= es enriched in bicategories. However, I only outlined a definition and only= briefly mentioned the context in which they arise. So I plan to give an ex= pository talk outlining a few of the one-dimensional generalisations of the= notion of category that have been studied over the past sixty years, with = an idea of how they arose and how they relate to each other.

** **

**16 May**

** Alessio Guglielmi =
(University of Bath)**<=
span style=3D"color: rgb(33,33,33);">In the past year we have obtained several results in deep inference,=
helped by a productive sabbatical for me. In my opinion, it is time to mak=
e an effort and push deep inference into the mainstream.

Sabbatical Report

In fact, I just found out that, co= ntrary to what I have been thinking so far, deep inference has dramatic, po= sitive consequences on the complexity of proofs above propositional logic. = Another reason is that we have now a theory of normalisation that is more p= owerful and is conceptually clearer than the traditional one.

I will give a high-level presentat= ion of the main results of the past year, which are: 1) subatomic logic and= a common structure behind normalisation procedures; 2) elimination of cycl= es and its impact on substitution theory; 3) a generalised understanding of= quantification and its impact on the complexity of proofs.

There are opportunities for severa= l projects that extend or apply those results, in particular on cyclic proo= fs, process algebras, the epsilon calculus, the Curry-Howard isomorphism (o= n which I recently changed my mind a bit), and more. It would be helpful fo= r me to get feedback on what the best strategy for future grant application= s could be.

I have been told by many experienc= ed colleagues that what is needed now, in order to make deep inference popu= lar, is a textbook. I am convinced that this is necessary and I believe tha= t the best way is to found the new theory starting from the notion of atomi= c flow. I will tell you what I think the atomic flows can and should do in = terms of foundations, but I need your help to approach them from the catego= rical point of view. (A categorical understanding of atomic flows is necess= ary because they basically are string diagrams, which are seemingly becomin= g the foundation for quantum theories, which in turn might benefit from the= compression and computation properties of deep inference.)

**2 May**

**John Power (University of Bath)**

Both finitary monads (easily) and Lawvere theories (with more effort) exten=
d from Set to arbitrary locally finitely presentable categories. So last ye=
ar in Sydney, Richard and I explored the extension of his construction via =
Cauchy completions. That works most naturally if one does it in a unified w=
ay, i.e., not for one locally finitely presentable category at a time, but =
for all simultaneously, using the notion of W-category for a bicategory 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 is much t=
o absorb, e.g, the concepts of Cauchy completion and categories enriched in=
bicategories. The emphasis will very likely be on Richard's work rath=
er than the work we did jointly.

** **

**28 March**

**John Power (University of Bath)**

A propositional logic program P may be identified with a (Pf Pf)-coalgebra =
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, describes deriv=
ations by resolution.That correspondence has been developed to model first-=
order programs in two ways, with lax semantics and saturated semantics, bas=
ed on locally ordered categories and right Kan extensions respectively. We =
unify the two approaches, exhibiting them as complementary rather than comp=
eting, reflecting the theorem-proving and proof-search aspects of logic pro=
gramming.

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

** **

**7 March**

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

Schanuel's conjecture is the centr= al, yet unsettled, proposition in transcendental number theory. Most of the= known results (like famous Lindemann-Weierstrass theorem) and other conjec= tures in this theory follow from Schanuel. The conjecture turned out to be = useful in model theory/analytic geometry, for example Macintyre and Wilkie = proved Tarski's conjecture on decidability of the theory of the reals with = exponentiation, assuming Schanuel. Recently I studied, with C. Riener, the = structure of irreducible components of real exponential sets, using Schanue= l. In this talk I will remind the basics of transcentental numbers, formula= te 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 bicategory: a b= icategory bears the same relationship to a 2-category as a monoidal categor= y bears to a strict monoidal category, a monoidal category being a one-obje= ct bicategory and a strict monoidal category being a one-object 2-category.=

It is not difficult to generalise the notion of 2-category to one of n-c= ategory for arbitrary n, but generalising the notion of bicategory has been= a focus of research in both category theory and algebraic topology since t= he 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 fe= w months, as we have gradually come to understand and, to some extent, reor= ganise the approach taken by Michael Batanin in Australia and Tom Lein= ster in Scotland.

Our work is not yet complete, but we believe it explicates a=
t least part of the underlying structure more clearly than hitherto done by=
using an enriched category theoretic perspective

**21 February**

**Marco Solieri (University of Bath)**

Models of efficient implementation= and fine semantics of higher order programming languages both need to include a formal account of&n= bsp;duplication. Once deconstr= ucted, duplication can then be:

* avoided - as in the static norma=
lisation of proof nets given by Girard's geometry of interaction (GoI);

* anticipated - as in the linearisation of lambda terms=
given by Taylor-Ehrhard-=
Regnier expansion;

* postpo=
ned - as in the optimal implementation of the lambda calculus <=
span style=3D"color: rgb(33,33,33);">given by Lamping's sharing graphs (SG)=
.

How the GoI and the Taylor expansi= on are related? Is the optimal implementation efficient? In this talk I will survey two of the = contributions I obtained in my= doctoral investigations, and sketch some the directions of my current or prospective interest.

I will first introduce the geometr= y of resource interaction, a GoI for the resource lambda calculus, that is the linear and non-determ= inistic variation of the = ordinary one being the domain of Taylor expansion. The algebraic structure which implements computat= ion on paths within a ter= m/proof correspond essentially to the multiplicative portion of the latter, enriched with a superpos= ition operator. An expanded version of Girard's execution formula can then be easily formulated and = shown to be invariant und= er reduction for ground-typed closed terms.

Secondly, I will recall that the o=
nly general (i.e. not empirical) result about the complexity of SG is restricted to two variants of&=
nbsp;linear logic proof-nets, =
ELL and LLL, which characterise two time

complexity classes, respectively elementary and polynomial. I=
n these cases, Baillot an=
d Dal Lago have shown exploiting a GoI-like approach that the complexity of SG remains in such compl=
exity classes. In the sam=
e setting, and together with Guerrini, I obtained a direct cost comparison between SG and the proof =
net reduction by purely syntactical means. A simulation between the two reductions allows to establi=
sh that a stronger 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 ty= pe system built on top of a typed programming language, as an extra layer of typing. Type refinement= systems in this sense ha= ve become increasingly popular, as a lightweight mechanism for improving the correctness of programs= . In the talk, I wi= ll give an introduction to a categorical perspective on type refinement systems that I have been dev= eloping in collaboration = with Paul-Andr=C3=A9 Melli=C3=A8s, based on the simple idea of modelling a = type refinement system as= an "erasure" functor from a category of typing derivations to a category of terms. Some quest= ions one can consider fro= m 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 derivation= ?

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

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

A particular class of type refinem= ent systems that are especially natural from this perspective are ones coming from a strict monoidal= closed functor that is s= imultaneously a bifibration. I will give some examples illustrating how such type refinement systems= can be used to give an a= xiomatic account of some phenomena from the semantics of separation logic and lambda calculus.

**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 proofs, has been applied to pr=
ogram semantics in mainly two styles. One style yields graph rewr=
iting systems for the lambda-calculus in which GoI gives an invariant =
of rewriting. The other style produces abstract machines that pass a t=
oken on a fixed graph along a path indicated by GoI. These styles=
of GoI in program semantics handle duplication of computation differe=
ntly with linear logic as a back end, and consequently can be efficien=
t in different ways.

The graph-rewriting GoI achieves time efficiency by=
copying subgraphs, whereas the token-passing GoI is space efficient b=
y repeating moves of a token in a fixed (sub)graph. Aiming at exp=
loring this spectrum of space and time efficiency, we introduce an abs=
tract machine called Dynamic GoI Machine (DGoIM). It combines graph re=
writing with token passing using a history of token passing.

We pro=
ve that the DGoIM can implement the call-by-need evaluation by interle=
aving token passing with as much graph rewriting as possible. Finally,=
we explore the tradeoffs of space and time cost in the DGoIM, by comp=
aring it with a variant of Danvy et al.'s call-by-need storeless abstr=
act machine.

The quantitative analysis confirms that these two machines =
have the same space efficiency (up to constant factors) and the DGoIM =
is more time efficient than the storeless abstract machine.

** **

__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 elimination p= rocedures for first-order theories provide a powerful tool for generically solving a wide range of p= roblems based on logical = specifications. In contrast to general first-order provers, quantifier = ;elimination procedures are ba= sed on a fixed set of admissible logical symbols with an implicitly fixed semantics. This admits the= use of subalgorithms from symbolic computation. We are going to start with traditional quantifier&n= bsp;elimination applied to ver= ification and simple problems from the life sciences. Beyond quantifier elimination we are going to = discuss recent results on an incomplete decision procedure for the existential fragment of the reals= , which has been successf= ully applied to the analysis of reaction systems in chemistry <= span style=3D"color: rgb(33,33,33);">and in the life sciences, which scales= to models currently used in systems biology. We might mention our open-source computer logic softwa= re Redlog, where our meth= ods are implemented (www.redlog.eu).

** **

**29 November**

**James Brotherston ( University College London)**

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

I describe array separation logic = (ASL), a variant of separation logic in which the data structures are eithe= r pointers or arrays. This logic can be used, e.g., to give memory safety p= roofs of imperative array programs.

The key to automatically inferring=
specifications is the so-called "*biabduction*" problem, given form=
ulas A and B, find formulas X and Y such that

A * X |=3D B * Y

(*and such that A * X is also s=
atisfiable*), where * is the well-known "separating conjunction" of sep=
aration logic. We give an NP decision procedure for this problem that=
produces solutions of reasonable quality, and we also show that the proble=
m of finding a consistent solution is NP-hard.

Along the way, we study satisfiabi= lity and entailment in our logic, giving decision procedures and complexity= bounds for both problems.

This is joint work with Nikos Goro=
giannis (*Middlesex*) and Max Kanovich (*UCL*). A paper=
describing the work is available at https://arxiv.o=
rg/abs/1607.01993 .

**22 November**

**Thomas Cottrell (University of Bath)**

Operads are tools for defining alg= ebraic structures in terms of the operations they have. In this talk, I wil= l describe the classical case of operads, in which each operation has a nat= ural number of inputs, called its arity. I will then explain how to general= ise this definition to allow for operads with more complex shapes of inputs= . Finally, I will show how these generalised operads can be used to define = weak n-categories, a very general type of higher-dimensional category.

**15 November**

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

From the outset, the global state = has been among the leading examples in the algebraic approach to computatio= nal effects. Indeed, the approach itself started from the recognition that = the global state admits a computationally natural presentation in terms of = operations and equations.

In this talk, I attempt to shed ne= w light on the global states by introducing a new class of computational ef= fects which I tentatively call `generalized global states'. First, I explai= n that the now standard presentation of the global state monad on Set (in t= erms of the update and lookup operations) is a particular instance of a muc= h more general phenomenon, whose first appearance essentially dates back to= Lawvere=E2=80=99s thesis. Second, I present a unified operational semantic= s for generalized global states and state a relationship to Plotkin and Pow= er's operational semantics based on effect values.

**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 continui= ty principle, saying that all functions (N->N)->N are continuous= , via the so-called Curry-Howard interpretation of logic, turns out to= be inconsistent. It becomes consistent under the univalent interpreta= tion of logic, which is similar to that of topos logic. In particular,= the notion of existence is interpreted as something strictly weaker than t= hat Martin-Loef's Sigma type, but stronger than its classical manifest= ation as the negation of a universal quantifier. In fact, the original= paper by Howard already points out that there are two natural constru= ctive 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 triviality in =
it. Paraconsistent logics are thus suited for reasoning in the presence of&=
nbsp;ineliminable inconsistencies, and they produce non-trivial but in=
consistent theories. There are two main philosophical traditions of studies=
of inconsistency and paraconsistent logic. One of them advocates for the p=
osition known as dialetheism: that some contradictions are tr=
ue, or, equivalently (given classical negation), that some propositions are=
both true and false. There is, however, another, somewhat earlier traditio=
n, which takes a very different approach to the matter of inconsistency. Th=
is tradition assumes, instead, paraconsistency to be a common trait of logi=
cs that are in some sense appropriate for situations of imperfect rationali=
ty or imperfect information. In particular, their research focuses on =
logics in which the presence of disagreement or misinformation can be expre=
ssed by a formal language itself. Collectively, the various logics develope=
d by this tradition and having such a property are known as logics=
of formal inconsistency. In my talk I shall briefly discuss the main differences that keep a=
part these two traditions of paraconsistency, with special attention to the=
different theoretical and practical problems they aim to solve. Then I sha=
ll focus on logics of formal inconsistency, taking the logic called * as my main example of the kind of behavior such logics exhi=
bit. I shall end with some remarks on the ongoing research in this traditio=
n of paraconsistency, as well as on its possible further developments.

**4 October**

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

The atomic lambda-calculus is known for its efficiency when evaluating t= erms; it is naturally fully lazy. Abstract machines are used to administer = evaluation strategies. In this talk, I will discuss the idea of building an= atomic abstract machine, implementing the evaluation strategy for the atom= ic lambda-calculus, with the intent of developing a fully lazy abstract mac= hine 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: trying to=
give a categorical understanding of atomic flows in order to study their a=
lgebra - in the technical sense of the term, that is the operations we can =
do with them. Apart from plugging together and juxtaposing two flows, Gugli=
elmi et al. proposed in an unpublished manuscript a notion of substitu=
tion of a flow inside a connected component of another, an operation which =
would generalise the usual notion of substitution of a formula inside the o=
ccurrences of an atom in another formula to that of substitution of a deriv=
ation inside the occurrences of an atom in another derivation. Categoricall=
y speaking, it seems that their idea can be formalised in terms of horizont=
al composition of families of morphisms, with which we interpret atomic flo=
ws. I will show how we generalised the well known definition of horizo=
ntal composition of natural transformations for a larger class of families =
of morphisms, namely extranatural transformations, in a meaningfu=
l way and what we have in mind to do for families of morphisms which a=
re obtained by composing natural and extranatural transformations,&nbs=
p;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 contextual equiva= lence in the untyped lambda-calculus, generated by taking the n= ormal forms as observables. Introduced by Morris in 1968, this is the = original extensional lambda theory H+ of observational equivalence. On= the syntactic side, we show that this lambda-theory validates the ome= ga-rule, thus settling a long-standing open problem. On the semantic s= ide, we provide sufficient and necessary conditions for relational gra= ph models to be fully abstract for H+. We show that a relational graph= model captures Morris's observational pre-order exactly when it is ex= tensional and lambda-K=C3=B6nig. Intuitively, a model is lambda-K=C3= =B6nig when every lambda-definable tree has an infinite path which 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 space. Inst= rumental for the presentation is Dana Scott's category Equ of equilogical s= paces. We present a subcategory of Equ, closed under the double exponential= 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 Abst= ract Stone Duality.

This is joint work with Giulia Frosoni a= nd Alessio Santamaria.

**20 April**

**Jamie Vicary (University of Oxford)**

Linear logic is a fundamental way to rea= son about resources that cannot be duplicated or deleted. In this talk, I w= ill present a new approach to the proof theory of linear logic, in which pr= oofs are represented as surfaces embedded in 3-dimensional space. Proof equ= ivalence then has a simple definition: two proofs are logically equivalent = just when their surfaces are geometrically equivalent. The technical basis = for the work comes from higher category theory, and I will give a simple an= d 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 notion of expressiveness for tempor= al logics that is based on game theoretic properties of multi-agent systems= . We focus on iterated Boolean games, where each player has a goal, represe= nted using (a fragment of) Linear Temporal Logic (LTL). This goal captures = the player's preferences: the models of the goal represent system behaviour= s that would satisfy the player. Moreover each player is assumed to act str= ategically, taking into account the goals of the other players, in order to= bring about computations satisfying their goal. In this setting, we apply = the standard game-theoretic concept of Nash equilibria: the Nash equilibria= of an iterated Boolean game can be understood as a (possibly empty) set of= computations, each computation representing one way the system could evolv= e if players chose strategies in Nash equilibrium. Such an equilibrium set = of computations can be understood as expressing a temporal property=E2=80= =94which may or may not be expressible within a particular LTL fragment. Th= e new notion of expressiveness that we study is then as follows: what LTL p= roperties are characterised by the Nash equilibria of games in which agent = goals are expressed in fragments of LTL? We formally define and investigate= this notion of expressiveness and some related 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. Shpilrain on a= novel approach to public key cryptography. These authors write: = ;

"We use various laws of classical physics to offer several = solutions of Yao=E2=80=99s millionaires=E2=80=99 problem without using= any one-way functions. We also describe several informationally secur= e public key encryption protocols, i.e., protocols secure against pass= ive computationally unbounded adversary. This introduces a new paradig= m of decoy-based cryptography, as opposed to =E2=80=9Ctraditional=E2= =80=9D complexity-based cryptography. In particular, our protocols do = not employ any one-way functions.=E2=80=9D

**5 April**

**Sam Staton (University of Oxford)**

I'll talk about the semantics of probabi= listic programming languages. This is an old subject, but recently probabil= istic programming has attracted a lot of interest as a method of stati= stical modelling, through languages like Anglican and Church. These raise s= ome new problems, such as how to combine continuous distributions with= higher types. I'll describe our work on operational semantics and den= otational semantics (based on sheaves and measurable spaces). <= /p>

**15 March**

**John Power (University of Bath) **

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

A propositional logic program P may be identified with a P<=
sub>fP_{f}-coalgebra on the set of atomic propositions 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<=
sub>f_{ }describes derivations by resolution. Using lax =
semantics, that correspondence may be extended to a class of first-order lo=
gic programs without existential variables. The resulting extension capture=
s 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. The motiva= tion for this construction is work arising from work by Laird and Churchill= in [1,2] concerning the sequoid operator. In [2], the authors constr= uct an exponential in the category of games that is a cofree commutative co= monoid for the 'tensor on the left' functor and a final coalgebra for the '= sequoid on the left' functor. In the category of finite games and str= ategies, this exponential can be constructed from the sequoid functor as th= e limit of a diagram indexed by the ordinal w. If we try to extend th= is result to the 'sequoidal categories' introduced in [1], then we find tha= t 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 sequ= oid using a suitable diagram indexed by k. Conversely, if a game cont= ains 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.

There is a sizeable body of research in the field of games = with plays indexed by transfinite ordinals (sometimes called 'long games').= In [3], Itay Neeman presents results concerning whether or not such = games are determined. More recently, Laird has applied a similar mode= l to the study of unbounded determinism in [4]. The construction give= n in this talk is a straightforward extension of the games model outlined i= n [1,5]. A nice feature of the construction is that it includes as sp= ecial cases both the 'games with winning condition on infinite plays', give= n in [5], and the pure finite games introduced by Blatt in [6].

After shifting focus from finite to infinite ordinals, it b= ecomes convenient to treat plays (ordinal sequences of moves), rather than = moves, as primitive, and one possible formulation is to define a game to be= a sheaf of sets on some given ordinal k, where the ordinal b < k is sen= t to the set of legal plays of length b. In contrast to the Abramsky-= Jagadeesan model, in which moves are designated as Player-moves or Opponent= -moves, we have a function that designates plays as Player-plays or Opponen= t-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 corresponds ex= actly to choosing a set of infinite plays that are Player-winning, as in [5= ].

I shall outline the motivation and construction for games p= layed over transfinite ordinals, and shall discuss briefly some tentative q= uestions about links to ordinals occurring elsewhere in the theory - in par= ticular, 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, J= une 2011

[2]: James Laird. A Categorical Semantics of Higher Order Store, C= TCS 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 Nondetermini= sm. MFPS XXXI: 271-287, 2015

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

[6]: A. Blass. A game semantics for linear logic. Annals 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 very recent= developments in linear logic proof nets.

__2015__

**8 December**

**Giuseppe Primiero (Middlesex University)**

Applications in computational domains complement verified knowledge with= information sharing processes. From a logical viewpoint, formulating asser= tion operations in terms of a trust function is challenging, both conceptua= lly and technically. In this talk we overview SecureND, a natural deduction= calculus for knowledge derivation under trust. Its design is motivated by = the problem of trust transitivity. We present also its implementation as th= e Coq protocol SecureNDC, to deal with trusted sources in software manageme= nt systems. We conclude with an overview of current and future extensions o= f our language.

** **

**1 December**

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

Through subatomic logic we are able to present sufficient c= onditions for a proof system to enjoy cut-elimination. In this talk I = will present subatomic logic, how it enables us to present proof systems th= at have single (linear) rule scheme and a recent result: we can genera= lise the splitting procedure for cut-elimination to any proof system w= hose rules and connectives have certain properties.

** **

**17 & 24 November**

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

I plan to give two talks about Lawvere theories. These= are not for experts but rather to give the details. Lawvere introduced the= notion in his PhD thesis in 1963, providing not only a category theoretic = account of universal algebra but one that is also presentation-independent.= Remarkably, his definition was embraced, albeit with a caveat and in diffe= rent terms, by universal algebraists but not by category theorists. The lat= ter, from 1966, generally preferred to model universal algebra owing to a l= ittle more generality but at a very considerable cost. Computer scientists = were then influenced to adopt monads, but much could and has been gained by= recasting some of the latter's concerns in terms of Lawvere theories. Ulti= mately, I think Lawvere theories are a superior approach, but benefit 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. W= e recently proposed a polarised, Curry-style approach to the =CE=BB-calculu= s with extensional sums, in correspondence with polarised intuitionist= ic logic. We suggested that associativity of composition in this conte= xt should not be seen as a syntactic axiom, but as an emergent propert= y akin to termination. Traditionally, issues with sums in denotational= semantics have rather been considered to be with extensionality than&= nbsp;with the associativity. This will be explained in an introductory fash= ion in a first part.

In a second part, I will more formally relate the termination in the&nbs= p;=CE=BB-calculus with sums to depolarisation, i.e. associativity of c= omposition, or more familiarly the fact that the order of evaluation d= oes not matter. First, a general setting of polarised realizability st= ructures for polarised calculi with or without control operators is develop= ed. Then, a general technique to build observational models from these= structures is explained. Finally, under broad conditions, the observa= tional models that the non-associative syntactic structure gives rise = to satisfy the associativity of composition (and are therefore cartesi= an closed categories with binary co-products). I will sketch an analog= y 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, providing compe= lling models for a strikingly wide range of programming languages, type the= ories and logics. A notable exception has been dependent type theory, which= had so far defied a game theoretic description. We present a proposal to f= ill this gap in the form of a new categorical model of dependent type theor= y, based on a category of games and history-free winning strategies. We mod= el dependent type theory with 1-, Sigma-, Pi- and intensional Id-types as w= ell as finite inductive type families (which act as ground types, like cale= ndars). 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 knowledge of gam= e 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 science, an= d randomized algorithms are the ones offering the best performances in many= domains. Higher-order probabilistic computation =E2=80=93 in which a proba= bilistic function may be passed as a parameter and returned as a result =E2= =80=93 is on the other hand a relatively underdeveloped field, which is how= ever receiving more and more attention. We give a survey of what is known a= bout probabilistic lambda-calculi, later focusing on some of our recent res= ults on implicit complexity and on inductive and coinductive techniques for= program equivalence. Finally, we hint at how all this could be useful when= structuring proofs of security for cryptographic primitives, but also 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 algorit= hms for the additive fragment of linear logic. This logic is an internal la= nguage for categories with finite sums and products, and describes concurre= nt two-player games of finite choice. In the context of session types, typi= ng disciplines for communication along channels, the logic describes the co= mmunication of finite choice along a single channel.

We give a simple linear time correctness criterion for unit-free proposi= tional additive proof nets via a natural construction on Petri nets. This i= s an essential ingredient to linear time complexity of the combinatorial pr= oofs for classical logic by Dominic Hughes.

For full propositional additive linear logic, including the units, we gi= ve a proof search algorithm that is linear-time in the product of the sourc= e and target formula, and an algorithm for proof net correctness that is of= the same time complexity. We prove that proof search in first-order additi= ve 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 arithmetic= to the language of monadic second-order logic (MSOL) completely axiomatise= s 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 var= ious classes of linear orders. Our proof formalises, in the axiomatisa= tion, a translation of MSO formulas to alternating parity tree automata. Th= e main ingredient is the formalised proof of positional determinacy for the= corresponding parity games which, as usual, allows us to complement automa= ta and to deal with the negation of MSO formulas. The Comprehension Scheme = of MSOL is used to obtain uniform winning strategies, whereas most usual pr= oofs of positional determinacy rely on instances of the Axiom of Choice or = transfinite induction. (Consequently we obtain an alternative decision proc= edure 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 presented = at LICS '15.

** **

**12 May**

** Georg Struth (University of Sheffield)**

Pomsets form a standard model of true concurrency. In this lecture I pre= sent a completeness result for a class of pomset languages, which generalis= es the regular languages to the realm of concurrency. More precisely I show= that the congruence on series-parallel rational pomset expressions generat= ed by series-parallel rational pomset language identity is axiomatised by t= he axioms of Kleene algebra plus those of commutative Kleene algebra. A dec= ision procedure is extracted from this proof. On the way to this result, se= ries-parallel rational pomset languages are proved to be closed under the o= perations of co-Heyting algebras and homomorphisms. These results form a si= gnificant step towards a decision procedure for the equational theory of co= ncurrent Kleene algebras, which have recently been proposed for concurrency= 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 conc= epts:

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

(2) validity in an intended class of models of separation logic, as comm= only considered in its program verification applications. Such intended cla= sses are usually specified by a collection of algebraic axioms describing s= pecific model properties, which we call a separation theory.

Here, we show first that several typical properties of separation theori= es are in fact not definable in BBI. Then, we show that these properties be= come definable in a natural hybrid extension of BBI, obtained by adding a t= heory of naming to BBI in the same way that hybrid logic extends normal mod= al logic. Finally, we show how to build an axiomatic proof system for our h= ybrid logic in such a way that adding any axiom of a certain form yields a = sound and complete proof system with respect to the models satisfying those= axioms. In particular, this yields sound and complete proof systems for an= y separation theory from our considered class (which, to the best of our kn= owledge, includes all those appearing in the literature).

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 language with= references (i.e. local mutable states) is a notoriously hard problem, spec= ially with higher-order references (i.e. references which can store functio= ns). In the last twenty years, different techniques have been introduce to = that purpose: Kripke Logical Relations, Bisimulations and Algorithmic 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 Laird, to = build a new technique, Kripke Open Bisimulations, to reason on equivalence = of programs, taking the best of the previous methods. This technique is sim= ple enough to be mostly automatized: it becomes possible to model-check equ= ivalence of programs.

If time permits, we will see how to extend this technique to polymorphis= m.

=20

=20
=20

=20
=20

=20
=20

=20
=20

=20