ScotCats 9: Fibrations in Computation Workshop

23rd – 24th June 2014.
Department of Computer and Information Sciences.

The idea of the workshop is to get people using fibrational methods in computer science together to catch up with what each of us is doing, to learn from each others techniques and to possibly chart ideas for future development and interaction.

This meeting is part of the Scottish Category Theory Seminar series.

Programme

Monday 23rd June

Time Talk
9:15 – 10:00 Operational Semantics for Logic Programming: embracing the laxness
John Power (Bath)
10:00 – 10:45 Fibrations, adjunctions and logical relations
Claudio Hermida
10:45 – 11:00 coffee
11:00 – 11:45 Fibrational Models for Stochastic Dynamics
Kohei Kishida (Oxford)
11:45 – 12:30 A self-dual approach to algebra using Grothendieck bifibrations
Thomas Weighill (Stellenbosch)
12:30 – 15:00 Lunch & time for work
15:00 – 15:45 Tangent bundles fibred over tangent categories are locally differential categories
Robin Cockett (Calgary)
15:45 – 16:30 Fibrational Units of Measure (slides)
Tim Revell (Strathclyde)
16:30 – 16:45 coffee
16:45 – 17.30 Coinductive Predicates and Final Sequences in a Fibration (slides)
Ichiro Hasuo (Tokyo)

Tuesday 24th June

Time Talk
9:15 – 10:00 A fibration of traces over configurations (slides)
Tom Hirschowitz (Savoy)
10:00 – 10:45 Bifibrational parametricity (slides)
Federico Orsanigo (Strathclyde)
10:45 – 11:00 coffee
11:00 – 11:45 Moens' theorem and fibered toposes (slides)
Jonas Frey (Cambridge)
11:45 – 12:30 Fibrations for conditional independence
Alex Simpson (Edinburgh)
12:30 – 15:00 Lunch & time for work
15:00 – 15:45 Coinduction up-to in a fibrational setting
Jurriaan Rot (Leiden)
15:45 – 16:30 Fibrations, view updates and lenses
Michael Johnson (Macquarie)

Abstracts

Filippo Bonchi (Lyon), Daniela Petrisan (Lyon), Damien Pous (Lyon), Jurriaan Rot (Leiden): Coinduction up-to in a fibrational setting
Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. We prove the soundness of such techniques in a fibrational setting, building on the seminal work of Hermida and Jacobs. This allows us to systematically obtain up-to techniques not only for bisimilarity but for a large class of coinductive predicates modelled as coalgebras. By tuning the parameters of our framework, we obtain novel techniques for unary predicates and nominal automata, a variant of the GSOS rule format for similarity, and a new categorical treatment of weak bisimilarity.
Robin Cockett (Calgary): Tangent bundles fibred over tangent categories are locally differential categories
Jonas Frey (Cambridge): Moens' theorem and fibered toposes (slides)

Let CC be a category with finite limits. Moens' theorem asserts an equivalence between the 2-category ExFib(CC) of extensive fibrations on CC, and the pseudo-co-slice category CC/Lex of finite-limit categories under CC. Under this equivalence, the fibration correspdonding to a functor F: CC → DD is the pullback of the codomain fibration of DD along FF, called gluing fibration of F.

In my talk, I want to explain how sheaf constructions and Grothendieck toposes relative to a base topos SS can be understood in terms of gluing fibrations and Moens' theorem, and how to generalize this framework to include realizability toposes.

Then I will describe how this point of view on realizability toposes allows to view them as cocompletions of generalized preorders (analogous to presheaves on meet-semilattices) and state an intrinsic characterization of realizability toposes over partial combinatory algebras, which arises quite naturally in this framework.

Claudio Hermida : Fibrations, adjunctions and logical relations
Ichiro Hasuo (Tokyo): Coinductive Predicates and Final Sequences in a Fibration (slides)
Tom Hirschowitz (Savoy): A fibration of traces over configurations (joint with Clovis Eberhart) (slides)
Motivated by game semantics, we construct a fibration from a `double factorisation system' (Tholen and Pultr) satisfying a few additional hypotheses. We construct a (pseudo) double category, using cospans whose legs satisfy certain factorisation properties. We show that the `vertical codomain' functor of this double category is then a fibration. Directed graphs will be used throughout as a stripped down example of a game.
Michael Johnson (Macquarie): Fibrations, view updates and lenses
Kohei Kishida (Oxford): Fibrational Models for Stochastic Dynamics
Federico Orsanigo (Strathclyde): Bifibrational parametricity (slides)
John Power (Bath): Operational Semantics for Logic Programming: embracing the laxness
Tim Revell (Strathclyde): Fibrational Units of Measure (slides)
In this talk I will give categorical semantics for Andrew Kennedy’s Units of Measure (1998). I'll start by following the standard approach in categorical logical and type theory by using a fibrational structure to separate index-information (the units) from indexed-information (the types which may contain units). This will lead us to the notion of a UoM-fibration. I'll give examples of UoM fibrations, including a model based upon G-sets, and theorems allowing the construction of further UoM-fibrations. Finally, I'll touch on parametricity in this setting.
Alex Simpson (Edinburgh): Fibrations for conditional independence
Thomas Weighill (Stellenbosch): A self-dual approach to algebra using Grothendieck bifibrations

In this talk we will discuss a new application of Grothendieck bifibrations in algebra. It relies on considering the bifibration of substructures of familiar group-like structures and reformulating standard results such as isomorphism theorems and diagram lemmas in terms of this bifibration, after which a completely self-dual approach to these results becomes possible using the intrinsic duality of the bifibrational language. This easily extends to categorical axiomatic contexts (where, as expected, substructures are traded for subobjects) studied in categorical and universal algebra, such as semi-abelian categories. Moreover, it becomes possible to characterise these contexts by dual axioms on the bifibration of subobjects [1]. We will then explain that one of the main ingredients of the theory is an additional 2-dimensional simplicial structure hidden behind the bifibration of subobjects in these categories. This work answers the proposal of Mac Lane in his paper Duality for Groups [4], namely that isomorphism theorems and similar results for groups be established in a self-dual categorical context. Pre-prints of two papers on this work are available [3,4].

[1] Z. Janelidze, On the Form of Subobjects in Semi-Abelian and Regular Protomodular Categories. Applied Categorical Structures (2013): 1-12
[2] S. Mac Lane, Duality for groups. Bulletin of the American Mathematical Society 56.6 (1950): 485-516.
[3] Z. Janelidze and T. Weighill, Duality in non-abelian algebra I. From cover relations to Grandis ex2-categories (submitted to Theory and Applications of Categories) preprint
[4] Z. Janelidze and T. Weighill, Duality in non-abelian algebra II. From Isbell bicategories to Grandis exact categories (submitted to Journal of Homotopy and Related Structures) preprint

Participants

  • Henning Basold
  • Filippo Bonchi
  • Robin Cockett
  • Jonas Frey
  • Neil Ghani
  • Giuseppe Greco
  • Ichiro Hasuo
  • Claudio Hermida
  • Tom Hirschowitz
  • Michael Johnson
  • Ohad Kammar
  • Ben Kavanagh
  • Kohei Kishida
  • Lorenzo Malatesta
  • Daniel Marsden
  • James McKinna
  • Fredrik Nordvall Forsberg
  • Federico Orsanigo
  • Daniela Petrisan
  • Damien Pous
  • John Power
  • Uday Reddy
  • Tim Revell
  • Jurriaan Rot
  • Alex Simpson
  • Fabio Zanasi
  • Thomas Weighill

Please let us know if you would like to attend (contact information below). The programme is now full, and we do not have time for any more talks.

Dinner

We are planning to go out for dinner Monday and Tuesday night: Here is a scanned copy of the receipt from Stravaigin.

Venue, Travel and Accommodation

The workshop will take place in room LT1415, on the 14th floor of Livingstone Tower, which is part of the University of Strathclyde. Livingstone Tower is in central Glasgow, near to both Glasgow Queen Street station and Glasgow Central Station. Below are travel instructions from the train stations, and from Glasgow and Edinburgh airports.

Map

The following map shows several key locations (click on the link below the map for a larger picture):


View a larger map.

Accommodation

A convenient place to stay is the Glasgow City Centre Premier Inn, just across the road from Strathclyde University.

From Glasgow Queen Street Station or Glasgow Central Station

Livingstone Tower is a few minutes walk from Queen Street Station in the centre of Glasgow, and about 10 minutes walk from Central Station. The map above shows the general area, as well as recommended walking routes.

There is also an official university map.

From Glasgow Airport

For people arriving at Glasgow Airport, here are instructions on how to get into the city centre. Probably the easiest route is to take the airport bus (Service 500) to Queen Street Station (or to stay on until Buchanan Street Bus station), and then to walk from there. The airport bus costs £7.50 for an open return.

From Edinburgh Airport

For people arriving via Edinburgh Airport, the best route is to take the airport bus to Buchanan Street Bus station in Glasgow, and then to walk or take a taxi from there. There are buses every 30 minutes during the day, and every hour after 19.30. The bus costs £16 for an open return. Here are general instructions on travel to and from Edinburgh airport.

Organisers

[SICSA logo]
This workshop is supported by the Scottish Informatics and Computer Science Alliance.