Categorical methods at the crossroads

Samson Abramsky works on computer science and category theory at Oxford. Together with Fabio Gadducci and Viktor Winschel (whom I didn't know), he's invited me to help organize a conference called “Categorical Methods at the Crossroads” at Schloss Dagstuhl. This is a castle in southwest Germany, or to be more precise in northern Saarland, near the French and Luxembourg borders, which somehow computer scientists have gotten their hands on.

I've accepted this invitation. The idea is that we'll write a proposal for a conference, and if it's accepted, the conference occur sometime in 2014. I hope it'll happen in the spring of 2014, since I seem to be planning to spend a few months in Europe then.

Here is a draft of the proposal that was given to me, in case anyone's interested.

Abstract. More than twenty years passed since “A categorical manifesto” by Joseph Goguen sketched some methodological guidelines for the application of categorical concepts to Computer Science, at the time still considered by the author “a field which is not yet very well developed”. Since then, CS has become pervasive in the whole of our society: in the meanwhile, it has refined its tools and blossomed into well-structured research areas, and the use of categorical methods and techniques has become accepted in some of them. Even if CT methods are part of the allowed frameworks for CS, its acceptance in conferences is hindered by the perceived difficulties of the formalism. Also, the lack of a venue precisely devoted to the presentation of current researches on CT applications to CS means the lack of an entry point for newcomers, as well as the lack of a meeting point for discussing and unifying the different research threads, since the single fields developed very specific instances of CT.

The same feeling is shared by other communities (mathematics, economics…), as proved by the different events organized on a “unifying platform”, such as the recent workshop on Category-Theoretic Foundations of Mathematics. The seminar should then help the reconciliation of different strands of research in CS that take their main tools from CT, as well as building bridges towards different fields, in order to foster cross-fertilisation.

This "recent workshop" is actually still forthcoming: Samson and I will be speaking there on 5-6 March at U. C. Irvine.

I think it's amusing how CS and CT sound like highly comparable entities in this abstract.

Goals of the seminar – Some research questions

The wide spectrum of disciplines and research themes that are potentially related to the application of categorical methods does not allow for a proper survey of all the relevant open issues in each areas. We are then going to offer just a sample of a few of the most successful recent threads of investigation.

CS: Presheaf semantics. The morphisms between two categories form themselves a category. Indeed, this simple remark has been the basis for one of the breakthrough of the last decade concerning the denotational semantics of nominal languages (e.g. with name passing, such as pi-calculus), nowadays one of the preferred formalisms for the specification of concurrent and distributed systems with a dynamically evolving topology. The paradigm has been proved able to cover a variety of languages and it has been applied also for the modelling of automata with infinite words/data types.

CS: coalgebraic logics. Coalgebras provided a neat charaterisation for the behavioural semantics of languages, e.g. as a suitable abstraction of the classical coinductive notion of bisimulation. However, it offered a suitable modelling environment for modal logics, and in general terms for those logics specifying properties of software systems with structured states specified by Kripke transition systems. The colagebraic framework proved a successful framework in addressing issues such as completeness, expressivity, and complexity for these logics, as witnessed also by two recent Dagtsuhl seminars.

CS/Physics: Quantum computing. A monoidal category can be succinctly described stating that its sets objects and arrows form monoids, subject to coherence laws. Such categories have been a staple for concurrency since their use for modelling Petri nets. Advocated as a domain for resource-aware logics (as linear logic), they provide a neat intermediate language for reconciling the two areas. Latest years have seen the use of these same tools (or enrichments, as the compact closed variant) for establishing a formal model of quantum computation and of some of its features, such as entanglement swapping.

CS/Economics: game theory. XXX

Economics: XXX

Physics: XXX

Mathematics: XXX

The XXX's are presumably things I should help fill in. I'm going to push for chemistry and biology to be added to this list.

Sign In or Register to comment.