Aim and scope

Dates

Programme

Invited speakers

Program committee

Steering committee

TMCNAA Programme, July 15-th, 2007

Abstracts

09:00-10:00: Samson Abramsky, Copy-cat Strategies and Information Flow in Physics, Geometry, Logic and Computation

Abstract:

10:10-10:30: Coffee break

10:30-11:15: Masahito Hasegawa, On Traced Monoidal Closed Categories.

Abstract: We discuss the relationship between traces and closed structure, with some applications. The structural theorem of Joyal, Street and Verity says that every traced monoidal category C arises as a monoidal full subcategory of the tortile monoidal category IntC. In this talk we focus on a simple observation that a traced monoidal category C is closed if and only if the canonical inclusion from C into IntC has a right adjoint. Thus, every traced monoidal closed category arises as a monoidal co-reflexive full subcategory of a tortile monoidal category. From this, we derive a series of facts on traced models of linear logic, and some on models of fixed-point computation. Interestingly, it can also be used for explaining some aspects of a program transformation technique recently developed by Nishimura and Katsumata.

11:15-12:00: Paulo Oliva, Hoare Logic in the Abstract.

Abstract: We present an abstraction of Hoare logic to traced monoidal categories. We first identify a particular class of monoidal functors -- which we call "verification functors" -- between traced monoidal categories and subcategories of PreOrd (the category of preordered sets and monotone mappings). Parametrised by a verification functor, we give an abstract definition of Hoare triples and a proof system, and prove a single soundness and completeness theorem for these. In the particular case of the traced monoidal category of while programs we get back Hoare's original rules. We discuss how our framework handles variants and extensions of the Hoare logic for while programs, e.g. total correctness, forward/backward reasoning, and the extension with pointer manipulations via separation logic. Finally, we discuss how our theory can be used in the development of new Hoare logics for other kind of system (such as continuous systems). [Joint work with U. Martin and E. A. Mathiesen]

12:00-12:05: Mini-break

12:05-12:30: Ross Duncan, Quantum Entanglement and Freely Constructed Compact Categories

Abstract: The categorical approach to quantum mechanics initiated by Abramsky and Coecke is based on \dag-compact categories. In this work I will characterise the free construction of such catgeories, based on a polycategory of basic interactions, and discuss the representation of entangled quantum states in this formalism.

12:30-14:00: Lunch

14:00-14:45: Prakash Panangaden, Traces, Kahn Networks and the Geometry of Interaction.

Abstract: Kahn networks are a type of asynchronous concurrent system. Each network is viewed as a collection of autonomous computing agents communicating by one-way, unbounded data channels. Each agent executes its own program and may communicate with other agents by sending data tokens along channels or reading tokens from incoming channels. In determinate Kahn networks, if an agent attempts to read a token from an incoming channel that has no data it suspends until data become available. Under these conditions an agent computes a continuous function from input token streams to output token streams. In this case there is a pleasant fixed-point denotational semantics.

If an agent can branch on availability of data, the system becomes indeterminate. Giving denotational semantics for indeterminate dataflow networks was a troublesome problem eventually solved independently - and in different ways - by a variety of researchers. Giving a fixed point presentation was even more vexing, though also eventually solved.

In this talk I will describe a category of Kahn processes and show that it is a traced monoidal category. I will sketch how one can give a relational model based on profunctors and show that this category of profunctors is also traced using a coend construction. Finally, I will show how by using a geometry of interaction construction one can model higher-order Kahn processes. This is joint work with Thomas Hildebrandt and Glynn Winskel.

14:45-15:30: Gheorghe Stefanescu, Streams, Network Algebras, and Interactive Systems.

Abstract: In this talk we start with a brief presentation of the "multiplicative" (or "wave") models for network algebras. In the case of deterministic systems, they consist of stream processing functions, while in the nondeterministic case, following an "oracle-based-approach", we use sets of streams processing functions. Axiomatizations for various classes of data-flow networks are presented.

Next, we look to a particular class of networks built up from split-merge connectors, only. We present a few partial results and state a conjecture which may lead to an axiomatization for this class of networks.

A model (consisting of "rv-systems" - "interactive systems with registers and voices"), a core programming language, several specification and analysis techniques appropriate for modeling, programming and reasoning about interactive computing systems have been recently introduced by Stefanescu (2004) using register machines and space-time duality.

In the final part of this talk we present preliminary results on the extension of network algebra formalism to rv-systems. Technically, rv-systems allow computation to extend both in space and in time and the proposed network algebra models are a kind of mixed, 2-dimensional extension of the one usual ones.

15:30-16:00: Coffee break

16:00-16:45: Gordon Plotkin, TBA

Abstract:

16:45-17:10: Peter Hines, The Trace and the Inverse: Iterative Traces in Inverse Categories.

Abstract: This talk is about the iterative or particle-style trace in inverse categories, treated as a form of conditional iteration that (unlike familiar programming languages constructs such as the While loop) preserves reversibility. The trace operation is shown to commute with the (generalised) inverse, and computational interpretations are considered. We then consider a construction that 'counts iterative cycles', and how this interacts with reversibility.

17:10-17:15: Mini-break

17:15-18:00: Dusko Pavlovic, Traces of intruders II: From Copy-cat, through Man-in-the-Middle, to Automated Turing Test

Abstract: I will show how traced monoidal categories, and the communication constructs that they support, provide a useful framework to model authentication protocols, and attacks on them. The monadic version of traces (presented in "Traces of intruders I", at the Fields Institute Workshop in April) provides a simplifying technical device.

18:00-18:45: Martin Hyland, Categorical Aspects of Traces

Abstract: I shall consider what we know about traces from the point of view of (groupoid enriched) categorical algebra. The natural issue is when and where we have monadicity. Traced monoidal categories are not monadic over categories. I shall discuss some consequences, and also information we have characterising the trace in special cases.