@techreport{Bundgaard:05:BigraphicalSemanticsOfHomerTR,
author = {Bundgaard, Mikkel and Hildebrandt, Thomas},
title = {Bigraphical Semantics of Higher-Order Mobile Embedded
Resources with Local Names},
institution = {IT University of Copenhagen},
year = 2005,
number = {TR-2005-70},
pdf = {http://itu.dk/people/mikkelbu/papers/ITU-TR-2005-70.pdf},
abstract = {\emph{Bigraphs} have been introduced with the aim to
provide a topographical meta-model for mobile,
distributed agents that can manipulate their own linkages
and nested locations, generalising both characteristics
of the $\pi$-calculus and the Mobile Ambients calculus.
We give the first bigraphical presentation of a
non-linear, higher-order process calculus with nested
locations, non-linear active process mobility, and local
names, the calculus of \emph{Higher-Order Mobile Embedded
Resources (Homer)}. The presentation is based on Milner's
recent presentation of the $\lambda$-calculus in local
bigraphs. The combination of non-linear active process
mobility and local names requires a new definition of
parametric reaction rules and a representation of the
location of names. We suggest \emph{localised bigraphs}
as a generalisation of local bigraphs in which links can
be further localised.}
}
@techreport{Bundgaard:07:SoftHardHomer,
author = {Bundgaard, Mikkel and Hildebrandt, Thomas and Godskesen, Jens Chr.},
title = {Typing Linear and Non-Linear Higher-Order Mobile Embedded
Resources with Local Names},
institution = {IT University of Copenhagen},
year = 2007,
number = {TR-2007-97},
pdf = {http://itu.dk/people/mikkelbu/papers/ITU-TR-2007-97.pdf},
abstract = {We provide the first process calculus combining
(affine) linear and non-linear higher-order mobile
processes, nested locations, and local names. We do
so by extending the type and effect system of Homer,
a calculus of non-linear Higher-Order Mobile
Embedded Resources, with a distinction between
affine linear and non-linear locations (akin to
reference types) and uses of variables (as in the
linear lambda calculus). The type system guarantees
that linear resources are neither copied nor
embedded in non-linear resources during computation.
We introduce composite reference types to guarantee
that no path ever points to a linear location nested
within a non-linear location. We extend the LTS
semantics and adapt Howe's method to the typed
setting, providing a bisimulation congruence. We
apply the bisimulation to prove that scope extension
across linear location boundaries is sound.
Finally, we use the calculus to model an e-cash
Smart Card system, the security of which depends on
the interplay between (linear) mobile hardware,
embedded (non-linear) mobile processes, and local
names.}
}
@techreport{Bundgaard:08:OnEncPiCalcInHOCalc,
author = {Bundgaard, Mikkel and Godskesen, Jens Chr. and Hildebrandt, Thomas},
title = {On Encoding the $\pi$-calculus in Higher-Order Calculi},
institution = {IT University of Copenhagen},
year = 2008,
number = {TR-2008-106},
pdf = {http://itu.dk/people/mikkelbu/papers/ITU-TR-2008-106.pdf},
abstract = {The connection between first-order calculi and
higher-order calculi have been examined in many
setting within the area of process calculi. In this
paper we examine two existing encodings of the
$\pi$-calculus in higher-order calculi: the encoding
in HO$\pi$-calculus by Sangiorgi and Walker and the
encoding in Plain CHOCS by Thomsen. We propose a
new encoding of the synchronous $\pi$-calculus in
the calculus of Higher-Order Mobile Embedded
Resources (Homer) inspired by the aforementioned
encodings. Homer is a pure higher-order calculus
with mobile processes in nested locations, defined
as a simple, conservative extension of the core
process-passing subset of Thomsen's Plain CHOCS.
Our encoding demonstrates that non-linear
higher-order process-passing together with mobile
resources in, possibly local, named locations are
sufficient to express $\pi$-calculus name-passing.}
}
@techreport{Hildebrandt:04:BisimCongruencesForHomer,
author = {Hildebrandt, Thomas and Godskesen, Jens Chr. and Bundgaard, Mikkel},
title = {Bisimulation Congruences for {H}omer --- a Calculus of Higher Order Mobile Embedded Resources},
institution = {IT University of Copenhagen},
year = 2004,
number = {TR-2004-52},
pdf = {http://itu.dk/people/mikkelbu/papers/ITU-TR-2004-52.pdf},
abstract = {We extend Howe's method for proving that late labelled
transition bisimulations are congruences to a core
process passing calculus with local names, extended with
non-linear active process mobility and nested locations,
as found in the Seal calculus, M-calculus, and
Kell-calculus. The calculus we consider, called Homer for
Higher-order Mobile Embedded Resources, has a very simple
syntax and semantics, which conservatively extend the
standard syntax and semantics for process passing
calculi. The extension of Howe's method gives a sound
characterisation of barbed bisimulation congruence in
terms of a late contextual bisimulation. We show that
early contextual bisimulation is complete with respect to
barbed bisimulation congruence, but that the late
bisimulation is in fact strictly included in the early
bisimulation. We discuss the issue of scope extension
through location boundaries in detail, in particular the
difference between fresh name generation and static local
names. We propose free name extension as a primitive
construct in calculi with non-linear process mobility,
explicit locations and local names.}
}
@techreport{Bundgaard:08:FormalBPELAndHOBPELinBigraph,
author = {Mikkel Bundgaard and Arne John Glenstrup and
Thomas Hildebrandt and Espen Højsgaard and
Henning Niss},
title = {Formalizing {WS-BPEL} and Higher Order Mobile Embedded Business Processes in the Bigraphical Programming Languages ({BPL}) {T}ool},
institution = {IT University of Copenhagen},
year = 2008,
number = {TR-2008-106},
pdf = {http://itu.dk/people/mikkelbu/papers/ITU-TR-2008-106.pdf},
abstract = {Bigraphical Reactive Systems (BRSs) have been
proposed as a formal meta-model for global
ubiquitous computing that encompasses process
calculi for mobility, notably the $\pi$-calculus and
the Mobile Ambients calculus, as well as graphical
models for concurrency such as Petri Nets. In this
paper we demonstrate that BRSs also allow natural
formalizations of programming languages used in
practice. We do so by providing a direct and
extensible formalization of a subset of WS-BPEL as a
binding bigraphical reactive system using the BPL
Tool developed in the Bigraphical Programming
Languages (BPL) project. The tool allows for
compositional definition, visualization and
simulation of the execution of bigraphical reactive
systems. The formalization exploits the close
correspondence between bigraphs and XML to provide a
formalized run-time format very close to standard
WS-BPEL syntax. The formalization is the starting
point of an endeavor to provide a completely
formalized and extensible business process engine
within the Computer Supported Mobile Adaptive
Business Processes (CosmoBiz) research project at
the IT University of Copenhagen. Building upon the
formalization of WS-BPEL we propose and formalize
HomeBPEL, a higher-order WS-BPEL-like business
process execution language where processes are
first-class values that can be stored in variables,
passed as messages, and activated as embedded
sub-instances. A sub-instance is similar to a
WS-BPEL scope, except that it can be dynamically
frozen and stored as a process in a variable, and
then subsequently be thawed when reactivated as a
sub-instance. We motivate HomeBPEL by an example of
pervasive health care where treatment guidelines are
dynamically deployed as sub processes that may be
delegated dynamically to other workflow engines and
in particular stay available for disconnected
operation on mobile devices.}
}
@techreport{Birkedal:09:HOContextViaGamesIntConstr,
author = {Lars Birkedal and Mikkel Bundgaard and S{\o}ren Debois and
Davide Grohmann and Thomas Hildebrandt},
title = {Higher-order Contexts via Games and the {I}nt-construction},
institution = {IT University of Copenhagen},
year = 2009,
number = {TR-2009-117},
pdf = {http://itu.dk/people/mikkelbu/papers/ITU-TR-2009-117.pdf},
abstract = {Monoidal categories of acyclic graphs capture the notion
of multi-hole context, pervasive in syntax and
semantics. Milner's bigraphs is a recent example. We
give a method for generalising such categories to
monoidal closed categories of acyclic graphs. The
method combines the Int-construction, lifting traced
monoidal categories to compact closed ones; the
recent formulation of sortings for reactive systems;
and games for multiplicative linear logic. The
closed categories obtained by our construction
captures a notion of higher-order contexts. These
encompass extensions to the traditional notion of
context found in recent work on Milner's reactive
systems and bigraphs. We demonstrate how technical
devices employed in these extensions are in fact
intrinsic to higher-order contexts. Finally, we use
the method to construct higher-order bigraphs,
recovering directed bigraphs as a limited instance.}
}
This file was generated by bibtex2html 1.96.