University of Birmingham > Talks@bham > Theoretical computer science seminar > The Berry Order (ideas from 1980s stable domain theory)

The Berry Order (ideas from 1980s stable domain theory)

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact George Kaye.

Zoom details


Besides Joyal’s “species”, the influences on work akin to polynomial functors in the 1980s were Diers’ “multiadjoints”, Berry’s initial investigations of “sequential programs” and Girard’s adaptation of this to the semantics of “System F”.

Using Berry’s term “stable domain theory”, Lamarche and I constructed numerous cartesian closed (bi)categories of categories and pullback-preserving functors, looking for better models of polymorphism.

In these, the order between maps is not pointwise but the “Berry order”; for categories the naturality squares must be pullbacks, so these were called “cartesian transformations”.

The function-spaces turn out to have a simpler representation than in “Scott” domain theory. This uses what Berry and Girard called the “trace”, which consists of the multiple universal (unit) maps from Diers’ theory, which I called “candidates”.

The one theorem that I shall prove is that the trace provides a factorisation system for stable functors. The “epis” are functors with (single) left adjoints and the “monos” are those which are equivalences on slices. The latter are essentially fibrations whose fibres are groupoids.

The different “flavours” of stable domains are measured by the properties of their slices (including familiar notions from categorical logic for no obvious reason) and the complexity of the “multicolimits” – both their cardinality and the kinds of groups that are involved.

A lot of this material was not written up properly, so there there is a goldmine waiting for younger researchers to develop. For example, Gabriel-Ulmer duality between LFP and lex categories can be extended to “disjunctive” theories. Also, the similarity between (bi)categories of domains and the domains themselves that was used to model System F might be adapted to finding models of univalence in HoTT.

Achim Jung has kindly agreed to chair this talk.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.