Abstracts

Abstracts

Departmental Seminar Thu December 4th, 16:00 Aula Verde.
Robin Cockett, University of Calgary, Restriction categories and the semantics of partiality.
Partial functions are absolutely fundamental in mathematics. They arise, for example, in elementary calculus. In fact, Karl Menger in his freshman calculus text (Menger 1955) already saw the need for a rigorous abstract theory of partiality. He and his students Bert Schweitzer and Abe Sklar subsequently developed an axiomatic theory for semigroups of partial functions (Menger 1959, Schweitzer and Sklar 1961,1967). Over the next fifty years this axiomatization was reinvented several more times both within semigroup theory and elsewhere.
Motivated by the work of Robert Di Paola and Alex Heller (Di Paolo and Heller 1987), Pino Rosolini and Edmund Robinson (Rosolini and Robinson 1988), and Aurelio Carboni (Carboni 1987), and completely unaware of the volume of work mentioned above Steve Lack and I provided (Cockett and Lack 2002) a categorical axiomatization of partiality which was almost identical to the above. In fact, even the name we chose, restriction} categories, had precedents in that literature. However, approaching the subject with categorical tools in hand allowed a much more perspicuous development of the subject than was hitherto possible.
In this talk I wish to introduce the basic theory of restriction categories. In particular, I will outline the completeness and representation theorems for these categories and discuss some (unlikely) examples. I will argue that restriction categories provide the cleanest basis, so far, for studying partiality. I will end by discussing some more recent developments. In particular, I would like to introduce Turing categories and the revamping of the theory of computability, which Pieter Hofstra and I are undertaking ... and why it is necessary.

Fri December 5th:
Session 1. Opening Session. 10:00 Aula Verde
10:00 Dr Kurt Ranalter, Queen Mary and UniVR, tba
10:45 Dr Graham White, Queen Mary UniLondon, Equational reasoning about the success or failure of actions
11:30 Dr Mehrnoosh Sadrzadeh, Oxford University What is the vector space content of what we say? A Categorical Approach to Meaning.
12:30 Robin Cockett, University of Calgary Turing categories.

Session 2. Categorical Logic.15:00 Aula Verde
15:00 Dr Eike Ritter, University of Birmingham, The Curry-Howard correspondence for modal System K revisited
The Curry-Howard isomorphism for intuitionistic modal logic S4 has been well established - there is both a well-established type theory and a well-established categorical semantics. In particular, fibrations can be used to model the distinction between modal and intuititonistic formulae.
For the weaker System K the situation is more complicated. There have been definitions of a suitable type theories and also categorical semantics, but a categorical semantics using fibrations in the same way as the one for intuitionistic S4 has not been given. We give such a categorical semantics and show that it also links in with the already existing type theories.

16:00 Dr Maria Emilia Maietti, University of Padova, Beyond soundness and completeness via category theory Categorical logic offers a way to strengthening the link given by the validity and completeness theorem of a calculus with respect to a class of models. This is achieved with the internal language theorem. As a consequence one is led to investigate the categorical connections among existing classes of complete models for a given calculus.
We exemplify such an analysis for some logical calculi including intuitionistic linear logic and some intuitionistic dependent type theories.
Ruggero Pagnan, University of Genova, Department of Computer Science, Relative factorization systems
The intended meaning of the in the title is with respect to a base category, in the sense of fibered category theory. We will introduce a notion of factorization system in a fibration which generalizes the usual one for categories in a non-trivial way. In particular, an application to descent theory will be described.

Sat December 6th: Session 3.
10:00 Dr Gianluigi Bellin An overview and some results in Logic and Pragmatics
11:00 Dr Mehrnoosh Sadrzadeh What is the vector space content of what we say? A Categorical Approach to Meaning.
12:00 Chistophe Raffalli On the lambda mu calculus and Montague grammars

back to the Workshop page