Seminar series of the Mathematical Foundations group at the University o= f Bath.
Tuesdays 13:15  15:05 in 1W 2.104
Seminars are open to all.
Organisers: Willem Heijltjes and Giulio Guerrieri
Email us to suggest speakers
Upcoming seminars
Informal Workshop Micro Structure and Deduction (MicroSD)

Program

Wednesday 29 May (Room 3W 3.7)
1:15 Adam La=
ssiter (Bath): Coalescence Proof Search for Classical Logic
2:00=
Michelangelo Mecozzi (Bath): Expansion Tree Proofs with Unification<=
br> 2:45  Coffee break 
3:15 Chris Barr=
ett (Bath): A Subatomic Proof System for Decision Trees
4:15&nbs=
p;  End (Pub!) 
Monday 3 June (Room 8W 1.33)
1:15 Delia Kesner (Paris 7): Principles of Quantitative =
Types for HigherOrder Languages
2:15 David Sherratt (Jena=
): The Spinal Atomic LambdaCalculus
2:45  Coffee break=

3:15 Giulio Guerrieri (Bath): Standardization via Lin=
ear Logic for CallbyName, CallbyValue and Choice Effects
4:0=
0 Benjamin Ralph (INRIA Paris): Towards a Combinatorial Proof Theory =
4:45  End (Pub?) 
<=
/p>
Abstracts
<=
br>
Wednesday 29th May, room 3W 3.7
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 2dimensional p= roduct space AxB 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 ndimensional coalescence  that is, there is some n such that A can b= e proved by coalescence over the space AxAx...xA (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)
E=
xpansion Tree Proofs with Unification
Expansion tree=
proofs are a representation of proofs in firstorder classical logic that =
is focused on the witnessing terms to existential quantifiers, factoring ou=
t both propositional proof content (which is decidable) and the bureaucracy=
of sequent calculus. They are based on Herbrand's theorem, and have a natu=
ral gamesemantic interpretation. There is also an interesting connection w=
ith learning algorithms.
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 firstorder 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 (Un=
iversity of Bath)
A Subatomic Proof System for Decision Trees<=
/em>
Recently, several proof systems have been developed =
in a very principled and regular way according to a methodology called 'sub=
atomic'. The main idea is to consider atoms as noncommutative selfdual co=
nnectives representing a superposition of truth values. This way, nonlinea=
r inference rules, such as contraction and cut, become linear and obey a un=
ique scheme. Normalisation is, therefore, at the same time, simplified and =
generalised. The contribution of this talk is that, surprisingly, by comple=
ting in the most natural way the standard subatomic proof system for propos=
itional classical logic, we obtain a new proof system for a conservative ex=
tension of propositional classical logic and of binary decision trees. Cut =
elimination for this system becomes an almost trivial variation of the alre=
ady known (and also trivial) 'experiment method', which is essentially a tr=
uth tabling operation that generates canonical analytic proofs.

Monday 3rd June, room 8W 1.33
=
Delia Kesner (Universit=C3=A9 de Paris, IRIF, CNRS)
Principles of Quantitative Types for HigherOrder 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. nonidempotent (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 Jena)
The Spinal Atomic LambdaCalculus
We introduce a variant of Gundersen, Heijltjes, and Parigot= 's atomic lambdacalculus. This typeable calculus with explicit sharing ext= ends the CurryHoward interpretation of open deduction already established&= nbsp;by the previous calculus. This expanded interpretation allow= s us to follow a duplication strategy stronger than full laziness, in = the sense that we duplicate less and share more of a term. This new ability= is strongly connected to interpreting the scopes of abstractions, whi= ch is strongly related to the open deduction system in turn. We estab= lish the good operational behaviour of the language by means of = some fundamental properties such as confluence and preservation of strong n= ormalisation. We finally discuss the possible benefits o= f this calculus, which may lead to some remarkable breakthroughs.

Giulio Guerrieri (University of Bath)
Standardization via Linear Logic for CallbyName, CallbyV= 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 lambdacalculus, LL provides a common setting where = both callbyname (CbN) and callbyvalue (CbV) evaluation mechanisms can b= e interpreted via Girard's translations. The bang calculus internalizes the= insights coming from LL proofnets into an untyped lambdalike 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 CallByPushValue 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 CallbyPush Value paradigm, as well = as related polarized calculi, admits LLbased models featuring nontrivial = computational effects such as nondeterministic 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, nondeterministic, or quantum). In = particular, we have a uniform method to study the fundamental syntactical r= esults for CbN and CbV lambdacalculi: confluence, standardization and norm= alization, and their extension to calculi with effects. Our approach allows= us not only to revisit some wellknown 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 ``syntaxf= 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 contractionweakening 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 settheoretic and graphtheoretic restrictions on the skew fibrat= ion, allowing us to characterise proof systems by their graph homomorphism = class.
Past seminars
2019
21st May (room 1W 3.107)
Cristina Matache (University of Oxford)
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 longstanding problem in computer science, made more difficult by the = presence of higherorder 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:
This work represents the first, fundamental steps towards a Godementlik= 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= nyvariable 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/03043975(90)901517.
[2] Girard, J.Y., Scedrov, A. and Scott, P.J., 1992. Normal Forms and C= utFree 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/9781461228226_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/03043975(93)90053V.
[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. Manyvariable 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)
Fibrations, approximations and intersection type syst=
ems (joint work with Damiano Mazza and<=
strong> Pierre Vial)<=
/span>
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 wellknown 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)
Intuit=
ionistic Proofs without Syntax (joint work with Dominic Hu=
ghes and Lutz Stra=C3=9Fburger)
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 cographs and coherence= spaces in classical and linear logic. Unlike game semantics, where arenas = are most often treelike, our arenas are DAGlike.
ICPs, like their classical counterparts, are then composed of two fragme= nts: a linear fragment called an "arena net", and a contractionweakening 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/nonlinear factorization is = at the formula level through the bang operator, ICPs factor at the level of= proofs, like Herbrand's Theorem for firstorder classical logic, and like = proof stratification in deep inference. An ICP can be viewed as a HylandOn= g strategy with additional sharing.
ICPs abstract fully and faithfully over all nonduplicating 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, lambdacalculus and game semantics incur an exp= onential blowup. This manifests in ICPs as a natural form of sharing, induc= ed by the DAGform of arenas.
We give a simple and direct normalization relation that arises naturally= from the semantics. It relates to closed reduction in lambdacalculus (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 callbyneed 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 CurryHoward 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 cutelimination 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= allbyvalue lambdacalculus crucially rely on the restriction to weak eval= uation and closed terms. Open callbyvalue 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 callby= value, adapting de Carvalho's analysis of callbyname via multi types (aka= nonidempotent 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 callbyvalue, 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 termforming 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 cutelimination
<=
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)
Categor=
y Theory of Computer Algebra
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)
Algeb=
raic methods for network diagrams and componentbased systems
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 resourceexchange between parts of
a system. This makes diagrammatic languages=
particularly effective in the analysis of subtle interactions as those fou=
nd in
cyberphysical, 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)=
Genericity Meets Dinat=
urality: The Semantics of Bounded Quantification
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 lambdacalculus) 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 subdeterminants 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)
PreLie Alge=
bras and Fmanifolds
The geometric notion of an Fmanif= old was introduced by Hertling and Manin as a natural generalisation of the= celebrated notion of a Frobenius manifold. Pointwise, the structure of an = Fmanifold 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 "Fmanifold algebras are infinitesimal preLie 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)
Linear Logi=
c and Session Types
In this talk, we first outline recent activities in our mobility gr= oup in
21 November
Hugo Paquet (University of Cambridge)
Probab=
ilistic Concurrent Game Semantics
Game semantics has been very succe= ssful at modelling the language PCF and various extensions. In particular, there is a fully abstract= games model (DanosHarme= 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.
7 November
Pawel Sobocinski (University of Southampton)
Graphical Linear Algebra
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
Combinatorial Flow=
s
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)
A =
compositional account of Herbrand's theorem via concurrent games
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 firstorder purely
existential formula =E2=88=83x.=CF=86(x)=
(with =CF=86 quantifierfree) 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 firstorder validity to propositional validity, by&n=
bsp;understanding the structure of the assignment of firstorder 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 firstorder 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 wellcho= 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 noncommutative sequoid operator =E2=8A=98 on games was intr= oduced to capture algebraically the presence of state in historysensitive = strategies in game semantics, by imposing a causality relation on the tenso= r product of games. Coalgebras for the functor A =E2=8A=98 _  i.e., m= orphisms from S to A =E2=8A=98 S  may be viewed as state transformers: if = A =E2=8A=98 _ has a final coalgebra, !A, then the anamorphism of such a sta= te transformer encapsulates its explicit state, so that it is shared only b= etween successive invocations.
When we use this construction to model stateful objects in game = semantics, we are using two properties of the game !A: firstly, that i= t is the final coalgebra for the functor A =E2=8A=98 _ (so that w= e may use it to encapsulate state) and secondly, that it is a model for the= exponential from linear logic (specifically, it is the cofree commutative = comonoid over A). I will investigate the underlying reasons why the s= ame object carries both structures by using the notion of a sequoidal categ= ory, which generalizes and formalizes the sequoid operator from games, and = discussing what extra conditions we need to place on it in order to guarant= ee that the final coalgebra for A =E2=8A=98 _ has the same = carrier as the cofree commutative comonoid over A.
I will give two different situations in which we can make this c= onclusion. The first is based upon the Melli=C3=A8sTabareauTas= son formula for the cofree commutative comonoid in the situation where it c= an be constructed as a sequential limit of symmetrized tensor powers. = ;The second approach adds the extra axiom that a certain isomorphism from != (A =C3=97 B) to !A =E2=8A=97 !B is an isomorphism. This sec= ond condition always holds in the case that !A is a bifree algebra for = ;A =E2=8A=98 _, but in general it is necessary to impose it, as we est= ablish by giving an example of a sequoidally decomposable category of games= in which plays will be allowed to have transfinite length. In this categor= y, the final coalgebra for the functor A =E2=8A=98 _ is not the cofree comm= utative comonoid over A: we illustrate this by explicitly contrasting the f= inal sequence for the functor A =E2=8A=98 _ with the chain of symmetric ten= sor powers used in the construction by Melli=C3=A9s, Tabareau and Tasson.
23 May
John Power (Univer=
sity of Bath)
Onedimensional generalisations of=
the notion of category
A few weeks ago, I gave a seminar on joint work with Richard Garner tha= t was based upon categories enriched in bicategories. However, I only outli= ned a definition and only briefly mentioned the context in which they arise= . So I plan to give an expository talk outlining a few of the onedimension= al generalisations of the notion of category that have been studied over th= e past sixty years, with an idea of how they arose and how they relate to e= ach other.
16 May
Alessio Guglielmi =
(University of Bath)
Sabbatical Report
In=
the past year we have obtained several results in deep inference, helped b=
y a productive sabbatical for me. In my opinion, it is time to make an effo=
rt and push deep inference into the mainstream.
In fact, I just found out = that, contrary to what I have been thinking so far, deep inference has dram= atic, positive consequences on the complexity of proofs above propositional= logic. Another reason is that we have now a theory of normalisation that i= s more powerful and is conceptually clearer than the traditional one.
I will give a highlevel p= resentation of the main results of the past year, which are: 1) subatomic l= ogic and a common structure behind normalisation procedures; 2) elimination= of cycles and its impact on substitution theory; 3) a generalised understa= nding of quantification and its impact on the complexity of proofs.<= /strong>
There are opportunities fo= r several projects that extend or apply those results, in particular on cyc= lic proofs, process algebras, the epsilon calculus, the CurryHoward isomor= phism (on which I recently changed my mind a bit), and more. It would be he= lpful for me to get feedback on what the best strategy for future grant app= lications could be.
I have been told by many e= xperienced colleagues that what is needed now, in order to make deep infere= nce popular, is a textbook. I am convinced that this is necessary and I bel= ieve that the best way is to found the new theory starting from the notion = of atomic flow. I will tell you what I think the atomic flows can and shoul= d do in terms of foundations, but I need your help to approach them from th= e categorical point of view. (A categorical understanding of atomic flows i= s necessary because they basically are string diagrams, which are seemingly= becoming the foundation for quantum theories, which in turn might benefit = from the compression and computation properties of deep inference.)<= /strong>
2 May
John Power (University of Bath)
28 March
John Power (University of Bath)
7 March
Nicolai Vorobjov (University of Bath)
=
Lindemann's Theorem and Schanuel's Conjecture
Schanuel's conjecture is t= he central, yet unsettled, proposition in transcendental number theory. Mos= t of the known results (like famous LindemannWeierstrass theorem) and othe= r conjectures in this theory follow from Schanuel. The conjecture turned ou= t to be useful in model theory/analytic geometry, for example Macintyre and= Wilkie proved Tarski's conjecture on decidability of the theory of the rea= ls with exponentiation, assuming Schanuel. Recently I studied, with C. Rien= er, the structure of irreducible components of real exponential sets, using= Schanuel. In this talk I will remind the basics of transcentental numbers,= formulate the conjecture and some of it's consequences.
28 February
John Power (University of Bath)
Clubs, enrichment and=
weak n categories: a progress report
In the early 1960's, Jean Benabou proposed the notion of bicateg= ory: a bicategory bears the same relationship to a 2category as a monoidal= category bears to a strict monoidal category, a monoidal category being a = oneobject bicategory and a strict monoidal category being a oneobject 2c= ategory.
It is not difficult to generalise the notion of 2category to on= e of ncategory for arbitrary n, but generalising the notion of bicategory = has been a focus of research in both category theory and algebraic topology= since the late 1980's, and it remains so now. Here, I report on = progress that Soichiro Fujii, Thomas Cottrell and I have made over the= past few months, as we have gradually come to understand and, to some exte= nt, reorganise the approach taken by Michael Batanin in Australia and = Tom Leinster in Scotland.
21 February
Marco Solieri (University of Bath)
<=
span style=3D"color: rgb(33,33,33);">The good, the bad and the ugly
Sharing, superpos=
ition and expansion in lambda terms and proof nets
Models of efficient implem= entation and fine semantics of higher order programming languages both need to include a formal acco= unt of duplication. Once = deconstructed, duplication can then be:
* avoided  as in the stat=
ic normalisation of proof nets given by Girard's geometry of interaction (GoI);
* anticipated  as in the linearisation of lamb=
da terms given by Taylor=
EhrhardRegnier expansion;
=
* postponed  as in the optimal implementation of the lambda calculus =
given by Lamping's sharing gra=
phs (SG).
How the GoI and the Taylor= expansion are related? Is the optimal implementation efficient? In this talk I will survey two of t= he contributions I obtain= ed in my doctoral investigations, and sketch some the directions of my current or prospective inte= rest.
I will first introduce the= geometry of resource interaction, a GoI for the resource lambda calculus, that is the linear and no= ndeterministic variation= of the ordinary one being the domain of Taylor expansion. The = algebraic structure which implements = computation on paths within a term/proof correspond essentially to the multiplicative portion of the= latter, enriched with a = superposition operator. An expanded version of Girard's execution formula can then be easily formula= ted and shown to be invar= iant under reduction for groundtyped closed terms.
Secondly, I will recall th=
at the only general (i.e. not empirical) result about the complexity of SG is restricted to two vari=
ants of linear logic proo=
fnets, ELL and LLL, which characterise two time
complexity classes, respectively elementary and polyn=
omial. In these cases, Ba=
illot and Dal Lago have shown exploiting a GoIlike approach that the complexity of SG remains in su=
ch complexity classes. In the same setting, and together with Guerrini, I obtained a direct cost&nbs=
p;comparison between SG and th=
e proof net reduction by purely syntactical means. A simulation between the two reductions allows to=
establish that a stronge=
r bound: a quadratic function.
7 February
Noam Zeilberger (University of Birmingham)
A Categorical Perspective on Type Refinement Sy=
stems
A "type refinement system"= is a type system built on top of a typed programming language, as an extra layer of typing. Type re= finement systems in this = sense have become increasingly popular, as a lightweight mechanism for improving the correctness of = programs. In the ta= lk, I will give an introduction to a categorical perspective on type refinement systems that I have = been developing in collaboration with PaulAndr=C3=A9 Melli=C3=A8s, based on the simple idea of mode= lling a type refinement s= ystem as an "erasure" functor from a category of typing derivations to a category of terms. So= me questions one can consider from this perspective include:
* What does it mean for a = program to have more than one type? What does it mean for a typing judgment to have more than one de= rivation?
* How should we understand= the socalled "subsumption rule"?
* If functors are type ref= inement systems, what does it mean for a functor to be a Grothendieck (bi)fibration?=
A particular class of type= refinement systems that are especially natural from this perspective are ones coming from a strict = monoidal closed functor t= hat is simultaneously a bifibration. I will give some examples illustrating how such type refinement= systems can be used to g= ive an axiomatic account of some phenomena from the semantics of separation logic and lambda calculu= s.
24 January
Koko Muroya (University of Birmingham)
Dynamic Geometry of Interaction machine: callbyne=
ed graph rewriter
Girard's Geometry of=
Interaction (GoI), that is semantics of Linear Logic pro=
ofs, has been applied to program semantics in mainly two =
styles. One style yields graph rewriting systems for the =
lambdacalculus in which GoI gives an invariant of rewrit=
ing. The other style produces abstract machines that pass=
a token on a fixed graph along a path indicated by GoI.<=
/span> These styles of GoI in program semantics handle duplicati=
on of computation differently with linear logic as a back=
end, and consequently can be efficient in different ways=
.
The graphrewriting GoI achieves time efficiency by copyi=
ng subgraphs, whereas the tokenpassing GoI is space effi=
cient by repeating moves of a token in a fixed (sub)graph=
. Aiming at exploring this spectrum of space and time eff=
iciency, we introduce an abstract machine called Dynamic =
GoI Machine (DGoIM). It combines graph rewriting with tok=
en passing using a history of token passing.We prove that the DGoIM can implement the callbyneed evaluation by interleaving token passing with as much graph rewriting as =
possible. Finally, we explore the tradeoffs of space and =
time cost in the DGoIM, by comparing it with a variant of=
Danvy et al.'s callbyneed storeless abstract machine.<=
/span>
The quantitative analysis confirms that these two machines =
have the same space efficiency (up to constant factors) a=
nd the DGoIM is more time efficient than the storeless ab=
stract 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 elimi= nation procedures for firstorder theories provide a powerful tool for generically solving a wide ra= nge of problems based on logical specifications. In contrast to general firstorder provers, quantif= ier elimination procedure= s are based on a fixed set of admissible logical symbols with an implicitly fixed semantics. This ad= mits the use of subalgorithms from symbolic computation. We are going to start with traditional quan= tifier elimination applie= d to verification and simple problems from the life sciences. <= span style=3D"color: rgb(33,33,33);">Beyond quantifier elimination we are g= oing to discuss recent results on an incomplete decision procedure for the existential fragment of t= he reals, which has been = successfully applied to the analysis of reaction systems in chemistry = and in the life sciences, whic= h scales to models currently used in systems biology. We might mention our opensource computer logi= c software Redlog, where = our methods are implemented (www.redlog.eu).
29 November
James Brotherston (University College London)
Biabduction (and Related Pr=
oblems) in Array Separation Logic
I describe array separatio= n logic (ASL), a variant of separation logic in which the data structures a= re either pointers or arrays. This logic can be used, e.g., to give memory = safety proofs of imperative array programs.
The key to automatically i= nferring specifications is the socalled "biabduction" problem, gi= ven formulas A and B, find formulas X and Y such that
A * X =3D B * Y
(and such that A * X i= s also satisfiable), where * is the wellknown "separating conjunction= " of separation logic. We give an NP decision procedure for this prob= lem that produces solutions of reasonable quality, and we also show that th= e problem of finding a consistent solution is NPhard.
Along the way, we study sa= tisfiability and entailment in our logic, giving decision procedures and co= mplexity bounds for both problems.
This is joint work with Ni= kos Gorogiannis (Middlesex) and Max Kanovich (UCL). = A paper describing the work is available at https:/= /arxiv.org/abs/1607.01993 .<= /span>
22 November
Thomas Cottrell (University of Bath)
Operads, generalised operads, and we=
ak ncategories
Operads are tools for defi= ning algebraic structures in terms of the operations they have. In this tal= k, I will describe the classical case of operads, in which each operation h= as a natural number of inputs, called its arity. I will then explain how to= generalise this definition to allow for operads with more complex shapes o= f inputs. Finally, I will show how these generalised operads can be used to= define weak ncategories, a very general type of higherdimensional catego= ry.
15 November
Soichiro Fujii (The University of =
Tokyo)
Generalized Global States
From the outset, the globa= l state has been among the leading examples in the algebraic approach to co= mputational effects. Indeed, the approach itself started from the recogniti= on that the global state admits a computationally natural presentation in t= erms of operations and equations.
In this talk, I attempt to= shed new light on the global states by introducing a new class of computat= ional effects which I tentatively call `generalized global states'. First, = I explain that the now standard presentation of the global state monad on S= et (in terms of the update and lookup operations) is a particular instance = of a much more general phenomenon, whose first appearance essentially dates= back to Lawvere=E2=80=99s thesis. Second, I present a unified operational = semantics for generalized global states and state a relationship to Plotkin= and Power's operational semantics based on effect values.<= /p>
1 November
Mart=C3=ADn Escard=C3=B3 (University of Birmingham)
C=
ontinuity in type theory
The formulation in MartinLoef type theory of a Brouwerian = continuity principle, saying that all functions (N>N)>N are co= ntinuous, via the socalled CurryHoward interpretation of logic, turn= s out to be inconsistent. It becomes consistent under the univalent in= terpretation of logic, which is similar to that of topos logic. In par= ticular, the notion of existence is interpreted as something strictly weake= r than that MartinLoef's Sigma type, but stronger than its classical = manifestation as the negation of a universal quantifier. In fact, the = original paper by Howard already points out that there are two natural= constructive notions of existence (a weak and a strong one).
25 October
Pedro Henrique Carrasqueira (CLE, University of Campinas=
, Brazil)
Some introductory remarks to paraconsistency and logics of for=
mal inconsistency
A logic is paraconsistent if inconsistencies do not imply trivia=
lity in it. Paraconsistent logics are thus suited for reasoning in the pres=
ence of ineliminable inconsistencies, and they produce nontrivia=
l but inconsistent theories. There are two main philosophical traditions of=
studies of inconsistency and paraconsistent logic. One of them advocates f=
or the position known as dialetheism: that some contradiction=
s are true, or, equivalently (given classical negation), that some proposit=
ions are both true and false. There is, however, another, somewhat earlier =
tradition, which takes a very different approach to the matter of inconsist=
ency. This tradition assumes, instead, paraconsistency to be a common trait=
of logics that are in some sense appropriate for situations of imperfect r=
ationality or imperfect information. In particular, their research foc=
uses on logics in which the presence of disagreement or misinformation can =
be expressed by a formal language itself. Collectively, the various logics =
developed by this tradition and having such a property are known as
4 October
David Sherratt (University of Bath)
Towards an atomic abstract machine
The atomic lambdacalculus is known for its efficiency when eval= uating terms; it is naturally fully lazy. Abstract machines are used to adm= inister evaluation strategies. In this talk, I will discuss the idea of bui= lding an atomic abstract machine, implementing the evaluation strategy for = the atomic lambdacalculus, with the intent of developing a fully lazy abst= ract machine and proving it to be effective.
Alessio Santamaria (University of Bath)
Looking for a=
categorical notion of substitution of atomic flows
In this talk I present the work I have done in my first year: tryi=
ng to give a categorical understanding of atomic flows in order to study th=
eir algebra  in the technical sense of the term, that is the operations we=
can do with them. Apart from plugging together and juxtaposing two flows, =
Guglielmi et al. proposed in an unpublished manuscript a notion of sub=
stitution of a flow inside a connected component of another, an operation w=
hich would generalise the usual notion of substitution of a formula inside =
the occurrences of an atom in another formula to that of substitution of a =
derivation inside the occurrences of an atom in another derivation. Categor=
ically speaking, it seems that their idea can be formalised in terms of hor=
izontal composition of families of morphisms, with which we interpret atomi=
c flows. I will show how we generalised the well known definition of h=
orizontal composition of natural transformations for a larger class of fami=
lies of morphisms, namely extranatural transformations, in a mean=
ingful way and what we have in mind to do for families of morphisms wh=
ich are obtained by composing natural and extranatural transformations=
, but themselves are neither of them.
12 May
Giulio Manzonetto (Universit=C3=A9 Paris XIII)
New Results on Morris's Observational Theory =
 The Benefits of Separat=
ing the Inseparable
We study the theory of contextua= l equivalence in the untyped lambdacalculus, generated by taki= ng the normal forms as observables. Introduced by Morris in 1968, this= is the original extensional lambda theory H+ of observational equival= ence. On the syntactic side, we show that this lambdatheory validates= the omegarule, thus settling a longstanding open problem. On the se= mantic side, we provide sufficient and necessary conditions for relati= onal graph models to be fully abstract for H+. We show that a relation= al graph model captures Morris's observational preorder exactly when = it is extensional and lambdaK=C3=B6nig. Intuitively, a model is lambd= aK=C3=B6nig when every lambdadefinable tree has an infinite path whi= ch is witnessed by some element of the model.
27 April
Pino Rosolini (University of Genoa)
=
Frames from topology, algebraically
We describe a connection between= frames and algebras for the double exponential monad on the Sierpinski spa= ce. Instrumental for the presentation is Dana Scott's category Equ of equil= ogical spaces. We present a subcategory of Equ, closed under the double exp= onential monad, on which the category of algebras is equivalent to that of = frames (and frame homomorphisms). I hope to connect this with Taylor's work= on Abstract Stone Duality.
This is joint work with Giulia F= rosoni and Alessio Santamaria.
20 April
Jamie Vicary (University of Oxford)
=
Geometrical Proofs for Linear Logic
Linear logic is a fundamental wa= y to reason about resources that cannot be duplicated or deleted. In this t= alk, I will present a new approach to the proof theory of linear logic, in = which proofs are represented as surfaces embedded in 3dimensional space. P= roof equivalence then has a simple definition: two proofs are logically equ= ivalent just when their surfaces are geometrically equivalent. The technica= l basis for the work comes from higher category theory, and I will give a s= imple and accessible introduction to this.
19 April
Paul Harrenstein (University of Oxford)
Expressiveness and Nash Equilibrium in Iterated B=
oolean Games
We introduce and investigate a novel noti= on of expressiveness for temporal logics that is based on game theoretic pr= operties of multiagent systems. We focus on iterated Boolean games, where = each player has a goal, represented using (a fragment of) Linear Temporal L= ogic (LTL). This goal captures the player's preferences: the models of the = goal represent system behaviours that would satisfy the player. Moreover ea= ch player is assumed to act strategically, taking into account the goals of= the other players, in order to bring about computations satisfying their g= oal. In this setting, we apply the standard gametheoretic concept of Nash = equilibria: the Nash equilibria of an iterated Boolean game can be understo= od as a (possibly empty) set of computations, each computation representing= one way the system could evolve if players chose strategies in Nash equili= brium. Such an equilibrium set of computations can be understood as express= ing a temporal property=E2=80=94which may or may not be expressible within = a particular LTL fragment. The new notion of expressiveness that we study i= s then as follows: what LTL properties are characterised by the Nash equili= bria of games in which agent goals are expressed in fragments of LTL? We fo= rmally define and investigate this notion of expressiveness and some relate= d issues, for a range of LTL fragments.
12 April
Harry Gunn (University of Bath, Masters Student)
Naturebased Cryptography
This is a review of several papers by G. Grigoriev and V. Shpilr= ain on a novel approach to public key cryptography. These authors wri= te:
"We use various laws of classical physics to offer = several solutions of Yao=E2=80=99s millionaires=E2=80=99 problem witho= ut using any oneway functions. We also describe several informational= ly secure public key encryption protocols, i.e., protocols secure agai= nst passive computationally unbounded adversary. This introduces a new= paradigm of decoybased cryptography, as opposed to =E2=80=9Ctraditio= nal=E2=80=9D complexitybased cryptography. In particular, our protoco= ls do not employ any oneway functions.=E2=80=9D
5 April
Sam Staton (University of Oxford)
Se=
mantics for probabilistic programming
I'll talk about the semantics of= probabilistic programming languages. This is an old subject, but recently = probabilistic programming has attracted a lot of interest as a method = of statistical modelling, through languages like Anglican and Church. These= raise some new problems, such as how to combine continuous distributi= ons with higher types. I'll describe our work on operational semantics and&= nbsp;denotational semantics (based on sheaves and measurable spaces). =
15 March
John Power (University of Bath)
Category theoretic semantics for theorem proving in logic pr=
ogramming: embracing the laxness
(joint with Ekaterina Komendantskaya)
A propositional logic program P may be identified w= ith a P_{f}P_{f}coalgebra on the set of atomic proposition= s in the program. The corresponding C(P_{f}P_{f})coalgebra= , where C(P_{f}P_{f}) is the cofree comonad on P_{f= }P_{f}_{ }describes derivations by resolution. Us= ing lax semantics, that correspondence may be extended to a class of first= order logic programs without existential variables. The resulting extension= captures proofs by termmatching 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 AbramskyJagadeesan games = model to allow sequences of moves indexed by transfinite ordinals. Th= e motivation for this construction is work arising from work by Laird and C= hurchill in [1,2] concerning the sequoid operator. In [2], the author= s construct an exponential in the category of games that is a cofree commut= ative comonoid for the 'tensor on the left' functor and a final coalgebra f= or the 'sequoid on the left' functor. In the category of finite games= and strategies, this exponential can be constructed from the sequoid funct= or as the limit of a diagram indexed by the ordinal w. If we try to e= xtend this result to the 'sequoidal categories' introduced in [1], then we = find that this construction does not always produce a final coalgebra, but = that for natural categories of games a similar construction using a higher = ordinal will work. If the lengths of plays in an ordinal game can be = bounded by a limit ordinal k then we may construct the final coalgebra for = the sequoid using a suitable diagram indexed by k. Conversely, if a g= ame contains plays greater than an ordinal k then the limit of the natural = diagram indexed by k does not have the natural structure of a coalgebra.&nb= sp;
There is a sizeable body of research in the field o= f games with plays indexed by transfinite ordinals (sometimes called 'long = games'). In [3], Itay Neeman presents results concerning whether or n= ot such games are determined. More recently, Laird has applied a simi= lar model to the study of unbounded determinism in [4]. The construct= ion given in this talk is a straightforward extension of the games model ou= tlined in [1,5]. A nice feature of the construction is that it includ= es as special cases both the 'games with winning condition on infinite play= s', given in [5], and the pure finite games introduced by Blatt in [6].&nbs= p;
After shifting focus from finite to infinite ordina= ls, it becomes convenient to treat plays (ordinal sequences of moves), rath= er than moves, as primitive, and one possible formulation is to define a ga= me to be a sheaf of sets on some given ordinal k, where the ordinal b < = k is sent to the set of legal plays of length b. In contrast to the A= bramskyJagadeesan model, in which moves are designated as Playermoves or = Opponentmoves, we have a function that designates plays as Playerplays or= Opponentplays. If a play is indexed by a limit ordinal, then it has= no last move, so this distinction is important. For example, in the = case of games played over the ordinal w + 1, we are free to specify whether= a play of length w should belong to Player or to Opponent, and this corres= ponds exactly to choosing a set of infinite plays that are Playerwinning, = as in [5].
I shall outline the motivation and construction for= games played over transfinite ordinals, and shall discuss briefly some ten= tative questions about links to ordinals occurring elsewhere in the theory =  in particular, gamevalue 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: = 6574, June 2011
[2]: James Laird. A Categorical Semantics of Higher Order = Store, CTCS 2002. Proceedings of CTCS '02, Elsevier, 2002
[3]: Itay Neeman. The Determinacy of Long Games. De = Gruyter Series in Logic and its Applications, 1972
[4]: James Laird. Sequential Algorithms for Unbounded Nond= eterminism. MFPS XXXI: 271287, 2015
[5]: Samson Abramsky, Radha Jagadeesan. Games and full com= pleteness for multiplicative linear logic. Journal of Symbolic Logic = 59 (02): 543574, 1994
[6]: A. Blass. A game semantics for linear logic. An= nals of Pure and Applied Logic, 56(13): 183  220, 1992
1 March
Willem Heijltjes (Univer=
sity of Bath)
Proof Net=
s and Complexity
In this talk I will give an overview of some recent and some ver= y recent developments in linear logic proof nets.
2015
8 December
Giuseppe Primiero (Middlesex University)
Applications in computational domains complement verified knowle= dge with information sharing processes. From a logical viewpoint, formulati= ng assertion operations in terms of a trust function is challenging, both c= onceptually and technically. In this talk we overview SecureND, a natural d= eduction calculus for knowledge derivation under trust. Its design is motiv= ated by the problem of trust transitivity. We present also its implementati= on as the Coq protocol SecureNDC, to deal with trusted sources in software = management systems. We conclude with an overview of current and future exte= nsions of our language.
1 December
Andrea Aler Tubella (University of Bath)
A generalised cutelimination procedure through subatomic=
logic
Through subatomic logic we are able to present suff= icient conditions for a proof system to enjoy cutelimination. In this= talk I will present subatomic logic, how it enables us to present proof sy= stems that have single (linear) rule scheme and a recent result: we ca= n generalise the splitting procedure for cutelimination to any proof syste= m whose rules and connectives have certain properties.
17 & 24 November
John Power (University of Bath)
Lawvere Theories
I plan to give two talks about Lawvere theorie= s. These are not for experts but rather to give the details. Lawvere introd= uced the notion in his PhD thesis in 1963, providing not only a category th= eoretic account of universal algebra but one that is also presentationinde= pendent. Remarkably, his definition was embraced, albeit with a caveat and = in different terms, by universal algebraists but not by category theorists.= The latter, from 1966, generally preferred to model universal algebra owin= g to a little more generality but at a very considerable cost. Computer sci= entists were then influenced to adopt monads, but much could and has been g= ained by recasting some of the latter's concerns in terms of Lawvere theori= es. Ultimately, I think Lawvere theories are a superior approach, but benef= it very much from the relationship with monads, and I duly plan to explain = it.
27 October
Guillaume MunchMaccagnoni (University of Cambridge)
Polarised realizability structures, models, and depolaris=
ation
Polarisation describes the presence of an evaluation order, and = is characterised denotationally by a nonassociativity of compositions= . We recently proposed a polarised, Currystyle approach to the =CE=BB= calculus with extensional sums, in correspondence with polarised intu= itionistic logic. We suggested that associativity of composition in th= is context should not be seen as a syntactic axiom, but as an emergent= property akin to termination. Traditionally, issues with sums in deno= tational semantics have rather been considered to be with extensionali= ty than with the associativity. This will be explained in an introduct= ory fashion in a first part.
In a second part, I will more formally relate the termination in= the =CE=BBcalculus with sums to depolarisation, i.e. associativity o= f composition, or more familiarly the fact that the order of evaluatio= n does not matter. First, a general setting of polarised realizability= structures for polarised calculi with or without control operators is= developed. Then, a general technique to build observational models fr= om these structures is explained. Finally, under broad conditions, the= observational models that the nonassociative syntactic structure giv= es rise to satisfy the associativity of composition (and are therefore= cartesian closed categories with binary coproducts). I will sketch a= n analogy between intuitionistic depolarisation and parametricity.
20 October
Matthijs V=C3=A1k=C3=A1r (University of Oxford)
Game Semantics for Dependent Types
Game semantics can act as a unifying semantic framework, providi= ng compelling models for a strikingly wide range of programming languages, = type theories and logics. A notable exception has been dependent type theor= y, which had so far defied a game theoretic description. We present a propo= sal to fill this gap in the form of a new categorical model of dependent ty= pe theory, based on a category of games and historyfree winning strategies= . We model dependent type theory with 1, Sigma, Pi and intensional Idty= pes as well as finite inductive type families (which act as ground types, l= ike calendars). We discuss the place of the Idtypes in the intensionality = spectrum as well as the strong completeness properties the model satisfies.=
Most of the talk should be understandable without prior knowledg= e of game semantics and dependent type theory.
15 October
Ugo dal Lago (Universit=C3=A1 di Bologna)HigherOrder Probabilistic Computation: Calculi, Observational Equiva=
lence, and Implicit Complexity
Probabilistic models are more and more pervasive in computer sci= ence, and randomized algorithms are the ones offering the best performances= in many domains. Higherorder probabilistic computation =E2=80=93 in which= a probabilistic function may be passed as a parameter and returned as a re= sult =E2=80=93 is on the other hand a relatively underdeveloped field, whic= h is however receiving more and more attention. We give a survey of what is= known about probabilistic lambdacalculi, later focusing on some of our re= cent results on implicit complexity and on inductive and coinductive techni= ques for program equivalence. Finally, we hint at how all this could be use= ful when structuring proofs of security for cryptographic primitives, but a= lso when expressing probabilistic models in the context of machine learning= .
10 June
Willem Heijltjes (University of Bath)
This is joint work with Dominic Hughes. We investigate efficient= algorithms for the additive fragment of linear logic. This logic is an int= ernal language for categories with finite sums and products, and describes = concurrent twoplayer games of finite choice. In the context of session typ= es, typing disciplines for communication along channels, the logic describe= s the communication of finite choice along a single channel.
We give a simple linear time correctness criterion for unitfree= propositional additive proof nets via a natural construction on Petri nets= . This is an essential ingredient to linear time complexity of the combinat= orial proofs for classical logic by Dominic Hughes.
For full propositional additive linear logic, including the unit= s, we give a proof search algorithm that is lineartime in the product of t= he source and target formula, and an algorithm for proof net correctness th= at is of the same time complexity. We prove that proof search in firstorde= r additive linear logic is NPcomplete.
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 secondorder ar= ithmetic to the language of monadic secondorder logic (MSOL) completely ax= iomatises the associated theory (SkS) over infinite trees. This continues a= line of work begun by B=C3=BCchi and Siefkes with axiomatisations of MSOL = over various classes of linear orders. Our proof formalises, in the ax= iomatisation, a translation of MSO formulas to alternating parity tree auto= mata. The main ingredient is the formalised proof of positional determinacy= for the corresponding parity games which, as usual, allows us to complemen= t automata and to deal with the negation of MSO formulas. The Comprehension= Scheme of MSOL is used to obtain uniform winning strategies, whereas most = usual proofs of positional determinacy rely on instances of the Axiom of Ch= oice or transfinite induction. (Consequently we obtain an alternative decis= ion procedure for MSOL over infinite trees, via proof search, that remains = entirely internal to the language.)
This talk is based on joint work with Colin Riba that will be pr= esented at LICS '15.
12 May
Georg Struth (University of Sheffield)
Pomsets form a standard model of true concurrency. In this lectu= re I present a completeness result for a class of pomset languages, which g= eneralises the regular languages to the realm of concurrency. More precisel= y I show that the congruence on seriesparallel rational pomset expressions= generated by seriesparallel rational pomset language identity is axiomati= sed by the axioms of Kleene algebra plus those of commutative Kleene algebr= a. A decision procedure is extracted from this proof. On the way to this re= sult, seriesparallel rational pomset languages are proved to be closed und= er the operations of coHeyting algebras and homomorphisms. These results f= orm a significant step towards a decision procedure for the equational theo= ry of concurrent Kleene algebras, which have recently been proposed for con= currency verification (joint work with Michael Laurence).
5 May
James Brotherston (University College London)
Parametric completeness for separation theories (via hybrid logic=
).
In this talk, we consider the logical gap between the following = two concepts:
(1) provability in a propositional axiomatisation of separation = logic, which is usually given by the bunched logic BBI; and
(2) validity in an intended class of models of separation logic,= as commonly considered in its program verification applications. Such inte= nded classes are usually specified by a collection of algebraic axioms desc= ribing specific model properties, which we call a separation theory.
Here, we show first that several typical properties of separatio= n theories are in fact not definable in BBI. Then, we show that these prope= rties become definable in a natural hybrid extension of BBI, obtained by ad= ding a theory of naming to BBI in the same way that hybrid logic extends no= rmal modal logic. Finally, we show how to build an axiomatic proof system f= or our hybrid logic in such a way that adding any axiom of a certain form y= ields a sound and complete proof system with respect to the models satisfyi= ng those axioms. In particular, this yields sound and complete proof system= s for any separation theory from our considered class (which, to the best o= f our knowledge, includes all those appearing in the literature).<= /p>
This is joint work with Jules Villard, now at Facebook.=
28 April
Guilhem Jaber (Queen Mary)
Reasoning=
on Equivalence of Stateful Programs with Operational Game Semantics
Contextual equivalence of programs written in a functional langu= age with references (i.e. local mutable states) is a notoriously hard probl= em, specially with higherorder references (i.e. references which can store= functions). In the last twenty years, different techniques have been intro= duce to that purpose: Kripke Logical Relations, Bisimulations and Algorithm= ic Game Semantics.
In this talk, we will see how to use operational game semantics,= namely the trace semantics for a language with references introduced by La= ird, to build a new technique, Kripke Open Bisimulations, to reason on equi= valence of programs, taking the best of the previous methods. This techniqu= e is simple enough to be mostly automatized: it becomes possible to modelc= heck equivalence of programs.
If time permits, we will see how to extend this technique to pol= ymorphism.