ABSTRACT. Conservation of data is an idea to build programming languages and hardware that support fixed-space programs: data cannot be created or destroyed. In this paper we give some motivations for this work and discuss some related ideas such as linearity and reversibility. We then give some examples of models of computation that can be adapted to work in this way. We conclude by discussing some ongoing work in this area.

ABSTRACT. Traditionally, semantic models of imperative languages use an auxiliary structure which mimics memory. In this way, ownerships and other encapsulation properties need to be reconstructed from the graph structure of such global memory. We present an alternative "syntactic" model where memory is encoded as part of the program rather than as a separate resource. This means that execution can be modelled by just rewriting source code terms, as in semantic models for functional programs. Formally, this is achieved by the block construct, introducing local variable declarations, which play the role of memory when their initializing expressions have been evaluated. In this way, we obtain a language semantics which is more abstract, and directly represents at the syntactic level constraints on aliasing, allowing simpler reasoning about related properties. We illustrate this advantage by expressing in the calculus the "capsule" property, characterizing an isolated portion of memory, which cannot be reached through external references. Capsules can be safely moved to another location in the memory, without introducing sharing. We state that the syntactic model can be encoded in the conventional one, hence efficiently implemented, and outline the proof that the dynamic semantics are equivalent.

ABSTRACT. Scoped channels, in the pi-calculus, are not nameable, as they are bound and subject to alpha-renaming. For program analysis purposes, however, to identify properties of these channels, it is necessary to talk about them. We present herein a method for uniquely identifying scoped channels.

ABSTRACT. Based on Gandy's principles for models of computation we give category-theoretic axioms describing locally deterministic updates to finite objects. Rather than fixing a particular category of states, we describe what properties such a category should have. The computation is modelled by a functor that encodes updating the computation, and we give an abstract account of such functors. We show that every updating functor satisfying our conditions is computable.

ABSTRACT. We study Topological Quantum Computing (TQC) from the perspective of computability theory with the aim of definining a formal system which is able to capture the computational features of TQC. We discuss the mathematical model for TQC, namely Modular Tensor Categories, and their suitability for the construction of a domain of denotational objects similar to the Scott domain of the lambda calculus. This leads us to believe that a formalism similar to the classical lambda calculus can be defined also for TQC.

ABSTRACT. The goal of this ongoing investigations is a more general, more flexible, and more precise generic language for describing algorithms than ordinary sequential abstract state machines. More general, since it will incorporate greater nondeterminism. More flexible, because it allows sequences of assignments in a single step. More precise, on account of the exact control over the order in which values are accessed and the number of times they each are.