| Philippa Gardner and Uri
Zarfaty. Local reasoning about tree
updates |
| Abstract: Separation Logic and
Context Logic have been used to reason locally about heap update and
simple tree update. We study local reasoning based on Context Logic
for a more realistic, local tree-update language which combines update
commands with queries. This combination results in updates at multiple
locations, which significantly affects the complexity of the
reasoning. |
| Daniele Varacca and
Nobuko Yoshida. Typed Event Structures and the
Pi-calculus |
| Abstract: We propose a
typing system for the true concurrent model of event structures that
guarantees the interesting behavioural properties known as conflict
freeness and confusion freeness. Conflict freeness is the
true concurrent version of the notion of confluence. A system is
confusion free if nondeterministic choices are localised and do not
depend on the scheduling of independent components. Ours is the first
typing system to control behaviour in a true concurrent model. To
demonstrate its applicability, we show that typed event structures
give a semantics of linearly typed version of the pi-calculi with
internal mobility. The semantics we provide is the first
event structure semantics of the pi-calculus and generalises Winskel's
original event structure semantics of CCS. |
| Daniela
Cancila, Furio Honsell and Marina Lenisa. Functors Defined by Values on
Objects |
| Abstract: Functors which are
determined, up-to natural isomorphism, by their values on
objects, are called DVO (Defined by Values on Objects). We
focus on the collection of polynomial functors on a category of sets
(classes), and we give a characterization theorem of the DVO
functors over such collection of functors. Moreover, we show that
the (kappa-bounded) powerset functor is not DVO. |
| Adam Antonik and Michael Huth. Efficient Patterns for Model Checking Partial State
Spaces in CTL & LTL |
| Abstract:
Compositional model checks of partial Kripke structures
are efficient but incomplete as they may fail to recognize that
all implementations satisfy the checked property. But
if a property holds for such checks, it will hold in all
implementations. Such checks are therefore
under-approximations. In this paper we determine for
which popular specification patterns, documented at
a community-led pattern repository, this under-approximation
is precise in that the converse relationship holds as well for
all model checks. We find that many such patterns are
indeed precise. Those that aren't lose precision because of a sole
propositional atom in mixed polarity. Hence we can compute, with
linear blowup only, a semantic minimization in the same
temporal logic whose efficient check renders the precise result
for the original imprecise pattern. Thus precision can be secured
for all patterns at low cost. |
| Stephen Brookes. Variables as resource for shared-memory programs:
semantics and soundness |
| Abstract:
Bornat, Calcagno and Parkinson recently introduced a logic for
partial correctness in which program variables are treated as
resources, generalizing earlier work based on separation logic and
permissions. An advantage of their approach is that it yields a logic
devoid of complex side conditions: there is no need to pepper the
inference rules with of programs that perform concurrent reads. We
provide a denotational semantics and a soundness proof for the
concurrent fragment of their logic, extending our earlier work on
concurrent separation logic to incorporate permissions in a natural
manner. |
| Gerard Allwein, Ira Moskowitz and Keye
Martin. Algebraic information theory for
binary channels |
| Abstract: We study the
algebraic structure of the monoid of binary channels and show that it
is dually isomorphic to the interval domain over the unit interval
with the operation from "Entropy as a fixed point." We show that the
capacity of a binary channel is Scott continuous as a map on the
interval domain and that its restriction to any maximally commutative
submonoid of binary channels is an order isomorphism onto the unit
interval. These results allows us to solve an important
open problem in the analysis of covert channels: a provably correct
method for injecting noise into a covert channel which will reduce its
capacity to any level desired in such a way that the practitioner is
free to insert the noise at any point in the system. |
| Nicola Mezzetti and Davide Sangiorge. Towards a calculus for wireless
systems |
| Abstract: In wireless systems,
the communication mechanism combines features of broadcast, synchrony,
and asynchrony. We develop an operational semantics for a
calculus of wireless systems. We present a Reduction Semantics and a
Labelledd Transition Semantics and prove a correspondence result
between them. We first consider a core calculus,
essentially with only the primitives for communication, and then a few
extensions. A major goal of the semantics is to describe the
forms of interferences among the activities of processes that are
peculiar of wireless systems. Such interferences occur when a location
is simultenously reached by two transmissions. |
| Paul
Levy. Monads and Adjunctions for Global
Exceptions |
| Abstract: In this paper, we
look at two categorical accounts of computational effects (strong
monad as a model of the monadic metalanguage, adjunction as a
model of call-by-push-value with stacks), and we adapt them
to incorporate global exceptions. In each case,
we extend the calculus with a construct, due to Benton and
Kennedy, that fuses exception handling
with sequencing. This immediately gives us an
equational theory, simply by adapting the equations for
sequencing. We study the categorical semantics of the
two equational theories. In the case of the monadic
metalanguage, we see that a monad supporting exceptions is a
coalgebra for a certain comonad. We further show,
using Beck's theorem, that, on a category with equalizers, the
monad constructor for exceptions gives all such
monads. In the case of call-by-push-value
(CBPV) with stacks, we generalize the notion of CBPV
adjunction so that a stack awaiting a value can deal both with a
value being returned, and with an exception being
raised. We see how to obtain a model of
exceptions from a CBPV adjunction, and vice versa by
restricting to those stacks that are homomorphic wrt
exception raising. |
| Eduardo Bonelli. The Linear Logical Abstract
Machine |
| Abstract: We derive an abstract
machine from the Curry-Howard correspondence with a sequent calculus
presentation of Intuitionistic Propositional Linear Logic. The states
of the register based abstract machine comprise a low-level code
block, a register bank and a dump holding suspended procedure
activations. Transformation of natural deduction proofs into our
sequent calculus yields a type-preserving compilation function from
the Linear Lambda Calculus to the abstract machine. We prove
correctness of the abstract machine with respect to the
standard call-by-value evaluation semantics of the Linear
Lambda Calculus. |
| Ingo Battenfeld. Computational Effects in Topological Domain
Theory |
| Abstract: This paper contributes
towards establishing the category QCB, of topological quotients of
countably based spaces, and its subcategory TP, of topological
predomains, as a flexible framework for denotational semantics of
programming languages. In particular, we show that both categories
have free algebras for arbitrary countable parametrised equational
theories, and are thus, following ideas of Plotkin and Power, able to
model a wide range of computational effects. Furthermore, we give an
explicit construction of the free algebras. |
| Matthew
Collinson and David Pym. Bunching for Regions
and Locations |
| Abstract: There are a
number of applied lambda-calculi in which terms and types are
annotated with parameters denoting either regions or locations in
machine memory. Such calculi have been designed with safe
memory-management operations in mind. It is difficult to
directly construct denotational models for existing calculi of this
kind. We approach the problem differently, by starting from a class of
mathematical models that describe some of the essential semantic
properties intended in these calculi. In particular, disjointness
conditions between regions (or locations) are implicit in many of the
memory-management operations. Bunched polymorphism provides
natural type-theoretic mechanisms for capturing the disjointness
conditions in such models. We illustrate this by extending the Basic
Disjointness Model of $\alphalambda$ with regions. We show how
additive and multiplicative polymorphic quantifiers are interpreted. A
locations model is a special case. In order to relate this
enterprise back to previous work on memory-management, we provide an
example in which the model is refined and used to provide a
denotational semantics for a language with explicit allocation and
disposal of regions. |
| Chris Heunen and Bart Jacobs. Arrows, like Monads, are
monoids |
| Abstract: Monads are by now
well-established as programming construct in functional
languages. Recently, the notion of `Arrow' was introduced by Hughes as
a analogue, not with one, but with two type parameters. It consists of
a binary operator on types with operations satisfying certain
equations. At first, these arrows may look somewhat arbitrary. Here we
show that they are categorically fairly civilised, by showing that
they correspond to monoids in suitable subcategories of bifunctors
(C^op) x C -> C. This shows that, at a suitable level of
abstraction, arrows are like monads -- which are monoids in categories
of functors C -> C. |
| Josh Berdine and Peter
O'Hearn. Strong Update, Disposal, and
Encapsulation in Bunched Typing |
| Abstract:
We present a bunched intermediate language for strong
(type-changing) update and disposal of first-order
references. In contrast to other substructural type
systems, the additive constructs of bunched types allow the
encapsulation of state that is shared by a collection of
procedures. |
| Weng Kin Ho. An Operational Domain-theoretic
Treatment |
| Abstract: We develop an
operational domain theory for treating recursive types. The principal
approach taken here deviates from classical domain theory in that
we do not produce the recursive types via usual inverse limits
constructions - we have it for free. By extending type
expressions to endofunctors on a apply techniques developed herein to
reason about FPC programs. |
| Mohamed El-Zawawy
and Achim Jung. Priestley duality for strong
proximity lattices |
| Abstract: In 1937
Marshall Stone extended his celebrated
representation theorem for Boolean algebras to
distributive lattices. In modern terminology, the
representing topological spaces are zero-dimensional
stably compact, but typically not Hausdorff. In 1970,
Hilary Priestley realised that Stone's topology could
be enriched to yield order-disconnected compact
ordered spaces. In the present paper, we
generalise Priestley duality to a representation
theorem for strong proximity lattices. For these
a ``Stone-type'' duality was given in 1995 in joint
work between Philipp Sünderhauf and the second
author, which established a close link between these
algebraic structures and the class of all stably
compact spaces. The feature which distinguishes the
present work from this duality is that the proximity
relation of strong proximity lattices is ``preserved''
in the dual, where it manifests itself as a form of
``apartness.'' This suggests a link with the work of
Giovanni Sambin on formal topologies which in this paper
we can only hint at. Apartness seems
particularly attractive in view of potential
applications of the theory in areas of semantics
where continuous phenomena play a role; there, it is
the distinctness between different states which is
observable, not equality. The idea of separating
states is also taken up in our discussion of possible
morphisms for which the representation theorem extends
to an equivalence of categories. |
| John Power. Semantics for local
computational effects |
| Abstract:
Starting with Moggi's work on monads as refined to Lawvere
theories, we give a general construct that extends denotational
semantics for a global computational effect canonically to yield
denotational semantics for a corresponding local computational
effect. Our leading example yields a construction of the usual
denotational semantics for local state from that for global
state. Given any Lawvere theory $L$, possibly countable and
possibly enriched, we first give a universal construction that extends
$L$, hence the global operations and equations of a given effect,
to incorporate worlds of arbitrary finite size. Then, making delicate
use of the final comodel of the ordinary Lawvere theory $L$, we
give a construct that uniformly allows us to model $block$, the
universality of the final comodel yielding a universal property of
the construct. We illustrate both the universal extension
of $L$ and the canonical construction of $block$ by seeing
how they work in the case of state. |
| Massimo Merro
and Corrado Biasi. On the observational theory
of the CPS-calculus |
| Abstract: We study
the observational theory of Thielecke's CPS-calculus, a target
language for CPS transforms designed to bring out the jumping,
imperative nature of continuation-passing. We define a labelled
transition system for the CPS-calculus from which we derive a (weak)
labelled bisimilarity that completely characterises Morris'
context-equivalence. We prove a context lemma showing that Morris'
context-equivalence coincides with a simpler context-equivalence
closed under a certain class of contexts. Then we profit of the
determinism of the CPS-calculus to give a simpler labelled
characterisation of Morris' equivalence, resembling Abramsky's
applicative bisimilarity. We enhance our bisimulation
proof-methods with up-to bisimilarity and up-to context
proof techniques. We use our bisimulation proof techniques to study
the algebraic theory of the CPS-calculus proving two new algebraic
laws that we conjecture cannot be derived using the original axiomatic
semantics for the CPS-calculus. Finally, we prove the full abstraction
of Thielecke's encoding of the CPS-calculus into a fragment of Fournet
and Gonthier's Join-calculus with single pattern
definitions. |