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.
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