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 lensesMichael 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:- Monday: The Dhabba, Indian cuisine.
- Tuesday: Stravaigin, Scottish cuisine.
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.
- General instructions on how to get into city centre
- Instructions on the bus service from the airport
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
- Neil Ghani, Strathclyde. Email: Neil.Ghani [at] cis.strath.ac.uk.
- Fredrik Nordvall Forsberg, Strathclyde. Email: Fredrik.Nordvall-Forsberg [at] strath.ac.uk.
- Henning Basold, Nijmegen. Email: H.Basold [at] cs.ru.nl.
![[SICSA logo]](sicsalogo.jpg)
This workshop is supported by
the Scottish Informatics and
Computer Science Alliance.