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.