My published work can be viewed as centering around one theme: What are the mathematical properties of some concrete model for a language or logic? There are two reasons for asking a question like that. For one, everything we find out about the model (in particular facts which are independent from the item to be modelled, at least at first sight) tells us something about the thing we're trying to reason about via its reflection in the model. Secondly, and more ambitiously, we can try to characterize the (mathematical) properties needed to obtain a model of a particular kind. Category theory is particularly useful when it comes to supplying answers of this kind. There are four 'centres' of activity I have visited so far:

*Domain Theory ·
Concurrency ·
Models for linear logic ·
Games*

Below, I explain what I've done in each of those in some detail; a list of publications without comments is available, too.

My research interests centre around the area between mathematics and (theoretical) computer science. Given the four topics mentioned above, it should come as no surprise that modelling of (programming) languages and logics is a good description of my area of work which provides more detail. I have spent some time thinking about issues of sequentiality, the computational content of classical logic, and other ways of describing categories of a more abstract nature which allow a comparison with game models. Most of those are continuing projects.

Back when I was a student at the Technical University
Darmstadt, there was (well, still is, with different participants
mostly these days) a group
working in domain theory where I was introduced to the field. My
diploma thesis **Bereiche und topologischer
Zusammenhang** is about characterizing the kinds of domains one can
obtain by taking all the connected closed subsets of certain
topological spaces.

Related work, where connectedness is replaced by a weaker concept can
be found in **Domains arising as algebras for power space
monads.** In: Journal of Pure and Applied Algebra 89
(1993), pp. 305--328.

I wrote my PhD thesis ** Algebras for
Generalized Power Constructions** as a member of the same
group, supervised by Klaus
Keimel and, although unofficially, Achim Jung. The underlying
idea is to find out what the so-called power
constructions for categories of domains and categories of
locales have in common (to justify giving them the same name). It
turns out that, going via topological spaces, they can be viewed as
giving the free semilattices of a particular kind as long as the
domains/locales in question are sufficiently continuous/locally
compact. This tells us that the kind of parallelism one can model
with these constructions is basically restricted to having a
non-deterministic 'or' command. Or, viewed the opposite way, any
language which can be faithfully modelled using these constructions
might as well just have a (finitary) choice operator as its source of
non-determinism.

Having finished my PhD, I spent a year at the School of Cognitive and Computing Sciences at the University of Sussex in Matthew Hennessy's group, where I had my first encounter with concurrency theory. Apart from learning a lot about this, I collaborated with Anna Ingólfsdóttir in a somewhat ambitious project of finding models for the so called observational (pre)congruence. As it turned out, domain theory just didn't give us a very good handle on this at all, and the resulting characterization is fairly syntactic in nature.

** A Fully Abstract Denotational Model for
Observational Precongruence**. In: Hans Kleine Büning, editor,
Proceedings of CSL '95, Paderborn, pp. 335--361, Volume
1092 of Springer Lecture Notes in Computer Science 1092, 1996. There
is an on-line previous version of this as a BRICS research series report.
A journal
version has appeared in Theoretical Computer
Science, Volume 254, pages 35-61.

Categorical models for linear logic have interested me for a while
now. I have written some notes which give a short introduction **What is
a categorical model of linear logic?****.**

Having gained an individual EU grant as part of the Human Capital and Mobility Framework I joined the Computer Laboratory at the University of Cambridge, joining the Theory and Semantics Group. The work on poset-valued sets arose from the observation that coherence spaces can be viewed as arising over the category of sets and relations via a three-valued logic, and the same holds true for the category of hypercoherences. This led to a construction which generalizes both those, delivering models of classical or intuitistionistic linear logic, and as a degenerate version one obtains phase spaces. A possible application is using a four-valued logic to arrive at a relatively simple model (in the spirit of coherence spaces) which will not validate mix, and where all constants are interpreted by different objects of the category. More generally, the framework allows picking various features the model should have (classical versus intuitionistic, what degree of collapse when it comes to units/the connectives), and a categorical model providing those arises being built over a poset model satisfying the same properties. Since these are much easier to construct, this method allows the tailor-made construction of categorical models for various flavours of linear logic. This started out as joint work with my co-author Valeria de Paiva and was later completed by myself after she had left Cambridge.

**Building models for Linear Logic.** In: Proc. of the
7th Conference on Algebraic Methodology and Software Technology
(AMAST '98), Springer LNCS 1548.

There's a journal version:

A. Schalk and V. de Paiva. **Poset-valued
sets, or, How to build models for Linear Logic**. In Theoretical Computer Science 315 (2004),
pp 83-107. Preprint versions in gzipped
postscript and pdf format.

Some of the work I've done with Martin Hyland is about
construction models for linear logic. An overview which discusses
four types of construction, but without any details, can be found in
**Abstract Games for Linear Logic. Extended Abstract**, 26pp
(despite the title).
It has apperead in the conference proceedings for CTCS '99, Volume 29
of Electronic
Notes in Theoretical Computer Science.

We now have a detailed account of two of these constructions.
(Double) Glueing and orthogonality categories are discussed in ** Glueing
and Orthogonality for Models of Linear Logic**, in pdf format,
and there is a summary of the self-dualization construction. We also
discuss how a number of familar models for linear logic can be seen
as arising from these construction. This paper has appeared in a
slightly different form as: M. Hyland and A. Schalk. **Glueing and
Orthogonality for Models of Linear Logic**. In Theoretical
Computer Science 294 (2003), pp. 183--231. A gentler
introduction to glueing can be found on the notes page.

Recently I have started doing some work with Dominic Hughes and my
student Robin
Houston on the question of what the right categorical universe
for Hughes/van Glabbeek MALL proof nets is. So far we've produced one
preprint entitled **Modelling Linear Logic
Without Units (Preliminary Results)**.

I have given an introductory mini-course on games for postgraduates in the departments of mathematics and computer science. I produced notes entitled Games for Semantics for this course. These are aimed at somebody who hasn't had any exposure to games at all and would like a detailed description of the various constructions, complete with pictures. I would very much appreciate any feedback regarding these notes and their readability as a stand-alone text.

At some point I was employed on an EPSCR project entiteld "Uniform Game Semantics for Computational Reasoning" working with Martin Hyland who is also a member of the the DPMMS). Some of our work over the past three years has been concentrating on finding an `abstract category of games'. The purpose of this is to provide categories which provide the good properties of categories of games while having less of an ad-hoc nature, and whose categorical properties are derivable from a base category via various constructions. Said constructions turn out to be useful in their own right -- in fact, many of them are generalizations of ones found in various models for linear logic.

This work is summarized in
**Abstract Games for Linear Logic. Extended Abstract**, 26 pp.
written jointly with Martin Hyland. It has apperead in the conference
proceedings for CTCS '99, Volume 29 of Electronic Notes in
Theoretical Computer Science. For some reason this
article (all of Volume 29) currently isn't available from the
Elsevier webpage, so I provide the preprint here.

Our paper in LICS 2002, **Games on
Graphs and Sequentially Realizable Functionals. Extended
Abstract**. In: Proc. Logic in Computer Science
2002, IEEE Computer Science Press, pp. 257--264. Also in pdf format.

We are currently working on further journal publications to cover the material in greater detail. These are currently in too draft-y a state to be inflicted on anybody but ourselves.

Together with my student JJ Palacios I have
looked at games which are connected with (non-filiform) concrete data
structures. Our first results were presented at CTCS2004 **Concrete
Data Structures as Games**. In: Proceedings of CTCS04,
Copenhagen, Volume 122 of Electronic Notes in Theoretical
Computer Science. The preliminary version (which apart from
lay-out is almost identical) is available in ps format.

- Don MacInnes has finished his PhD successfully, writing a thesis on free constructions for lattices and ordered sets.
- JJ Palacios has graduated with a PhD; in his thesis he explores the world of event structures.
- Robin Houston recently finished his PhD. Both his PhD thesis `Linear Logic without Units' and his MSc dissertation `Categories of Games' are available online.

19 March 2008