@inproceedings{Bundgaard:05:ACPSEncNamePassingHOMER,
author = {Bundgaard, Mikkel and Hildebrandt, Thomas and Godskesen, Jens Chr.},
title = {A {CPS} Encoding of Name-Passing in Higher-Order Mobile Embedded Resources},
booktitle = {Proceedings of the 11th International Workshop on Expressiveness in Concurrency (EXPRESS'04)},
editor = {Baeten, Jos and Corradini, Flavio},
year = 2005,
volume = 128,
number = 2,
pages = {131--150},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
doi = {10.1016/j.entcs.2004.11.033},
pdf = {http://itu.dk/people/mikkelbu/papers/express04.pdf},
slides = {http://itu.dk/people/mikkelbu/papers/express04.slides.pdf},
abstract = {We present an encoding of the synchronous
$\pi$-calculus in the calculus of Higher-Order
Mobile Embedded Resources (Homer), 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. We prove that our encoding is
fully abstract with respect to barbed bisimulation
and sound with respect to barbed congruence. Our
encoding demonstrates that higher-order
process-passing together with mobile resources in
(local) named locations are sufficient to express
$\pi$-calculus name-passing. The encoding uses a
novel continuation passing style to facilitate the
encoding of synchronous communication.}
}
@inproceedings{Bundgaard:07:ModelSecurOfSmartCards,
author = {Bundgaard, Mikkel and Hildebrandt, Thomas and Godskesen, Jens Chr.},
title = {Modelling the Security of Smart Cards by Hard and Soft Types for Higher-Order Mobile Embedded Resources},
booktitle = {Proceedings of the 5th International Workshop on
Security Issues in Concurrency (SecCo'07)},
pages = {23--38},
year = 2007,
editor = {Gorla, Daniele and Palamidessi, Catuscia},
volume = 194,
number = 1,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
doi = {10.1016/j.entcs.2007.09.011},
pdf = {http://itu.dk/people/mikkelbu/papers/secco07.pdf},
abstract = {We provide a type system inspired by affine
intuitionistic logic for the calculus of
Higher-Order Mobile Embedded Resources (Homer),
resulting in the first process calculus combining
affine linear (non-copyable) and non-linear
(copyable) higher-order mobile processes, nested
locations, and local names. The type system
guarantees that linear resources are neither copied
nor embedded in non-linear resources during
computation. We exemplify the use of the calculus
by modelling a simplistic 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. A
purely linear calculus would not be able to express
that embedded software processes may be
copied. Conversely, a purely non-linear calculus
would not be able to express that mobile hardware
processes cannot be copied.}
}
@phdthesis{Bundgaard:07:SemanticsOfHomer,
author = {Bundgaard, Mikkel},
title = {Semantics of Higher-Order Mobile Embedded Resources and Local Names},
school = {IT University of Copenhagen},
year = 2007,
pdf = {http://itu.dk/people/mikkelbu/papers/mikkelBundgaardPhDThesis.pdf},
abstract = {We begin by presenting a process calculus that
focuses on the following key concepts: linear and
non-linear process-passing; named, nested locations;
and local names. These concepts are well-known and
well-understood in the `concurrency and mobility'
community, but the combination of them proposes new
challenges. In particular, scope extension across
location boundaries requires special care. We call
the process calculus Higher-Order Mobile Embedded
Resources and abbreviate it Homer. We examine the
expressive power of Homer and whether name-passing
can be a derived notion in Homer by giving an
encoding of the synchronous $\pi$-calculus in
Homer. The encoding establishes that process-passing
together with mobile resources in, possibly local,
named locations are sufficient to express
$\pi$-calculus name-passing. We provide Homer with
a type system for distinguishing between (affine)
linear and non-linear higher-order mobile processes
by assigning types to locations, names, and
variables. The type system is inspired by the
linear $\lambda$-calculus and by ideas from
reference types. We investigate the behavioural
theory of Homer by equipping the calculus with
behavioural congruences defined on top of the
reaction semantics through the usage of barbs. We
then proceed to provide the behavioural congruences
with sound and complete coinductive
characterisations using labelled context
bisimulations. We thereby provide the first sound
and complete characterisation of a behavioural
congruence for a calculus combining non-linear and
linear process-passing. We utilise the method of
Howe to prove that labelled context bisimulations
are congruences. As a technical contribution we
apply the bisimulation to prove that scope extension
across linear location boundaries is sound. The
meta-model of bigraphical reactive systems has been
proposed by Milner as a unifying meta-model for
representing process calculi for concurrency and
mobility. We evaluate the applicability of
bigraphical reactive systems by giving a bigraphical
semantics of Homer. The presentation of Homer as a
bigraphical reactive system again highlights the
issues with scope extension across location
boundaries and the locality of a name. The
presentation requires that we refine the definition
of parametric reaction rules to keep explicit track
of the locality of names. We end this dissertation
with an investigation of the connection between type
systems for process calculi and sortings for
bigraphical reactive systems. Concretely, we examine
an encoding of a typed $\pi$-calculus in a sorted
bigraphical reactive system. Using the theory of
bigraphical reactive systems we obtain a coinductive
characterisation of a behavioural congruence for the
calculus.}
}
@inproceedings{Birkedal:06:BPLForPervasiveComputing,
author = {Birkedal, Lars and Bundgaard, Mikkel and Damgaard, Troels
C. and Debois, S{\o}ren and Elsborg, Ebbe and
Glenstrup, Arne John and Hildebrandt, Thomas and
Milner, Robin and Niss, Henning },
title = {Bigraphical Programming Languages for Pervasive
Computing},
booktitle = {Proceedings of the 1st International Workshop on
Combining Theory and Systems Building in Pervasive
Computing},
pages = {653--658},
year = 2006,
editor = {Strang, Thomas and Cahill, Vinny and Quigley, Aaron},
pdf = {},
abstract = {The Bigraphical Programming Language project at IT
University of Copenhagen contributes to the UKCRC
Ubiquitous Computing Grand Challenge by researching
the use of bigraphical reactive systems as a general
framework in which to combine theories for design
and analysis with techniques, tools and
methodologies for engineering and systems
building. Initial work has been addressing
\emph{Context-awareness}, \emph{business processes
and Reactive XML}, \emph{axiomatisation and
matching}, and \emph{higher-order mobile embedded
resources}.}
}
@inproceedings{Bundgaard:06:TypedPolyadicPiCalculusInBigraphs,
author = {Bundgaard, Mikkel and Sassone, Vladimiro},
title = {Typed Polyadic Pi-calculus in Bigraphs},
booktitle = {Proceedings of the 8th ACM SIGPLAN international conference on Principles and Practice of Declarative Programming (PPDP'06)},
pages = {1--12},
year = 2006,
publisher = {ACM Press},
doi = {},
pdf = {http://itu.dk/people/mikkelbu/papers/ppdp06.pdf},
slides = {http://itu.dk/people/mikkelbu/papers/ppdp06.slides.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
communication links and nested locations. In this paper
we examine a presentation of type systems on bigraphical
systems using the notion of sorting. We focus our
attention on the \emph{typed polyadic $\pi$-calculus} with
capability types \`a la Pierce and Sangiorgi, which we
represent using a novel kind of link sorting called
\emph{subsorting}. Using the theory of \textit{relative
pushouts} we derive a labelled transition system which
yield a coinductive characterisation of a behavioural
congruence for the calculus. The results obtained in
this paper constitute a promising foundation for the
presentation of various type systems for the (polyadic)
$\pi$-calculus as sortings in the setting of bigraphs.}
}
@inproceedings{Bundgaard:05:AnEncodingOfHomerInBigraphs,
author = {Bundgaard, Mikkel and Hildebrandt, Thomas},
title = {Bigraphical Semantics of Higher-Order Mobile Embedded
Resources with Local Names},
booktitle = {Proceedings of the Graph Transformation for Verification and Concurrency workshop (GT-VC'05)},
pages = {7--29},
year = 2006,
editor = {Rensink, Arend and Heckel, Reiko and K{\"o}nig, Barbara},
volume = 154,
number = 2,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
doi = {10.1016/j.entcs.2005.03.029},
pdf = {http://itu.dk/people/mikkelbu/papers/gt-vc05.pdf},
slides = {http://itu.dk/people/mikkelbu/papers/gt-vc05.slides.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.}
}
@article{Bundgaard:05:ACPSEncNamePassingHOMERTCS,
author = {Bundgaard, Mikkel and Hildebrandt, Thomas and Godskesen, Jens Chr.},
title = {A {CPS} Encoding of Name-Passing in Higher-Order Mobile Embedded Resources},
journal = {Theoretical Computer Science},
year = 2006,
volume = 356,
number = 3,
pages = {422--439},
publisher = {Elsevier},
doi = {10.1016/j.tcs.2006.02.006},
pdf = {http://itu.dk/people/mikkelbu/papers/namePassingTCS.pdf},
abstract = {We present an encoding of the synchronous $\pi$-calculus
in the calculus of Higher-order mobile embedded
resources (Homer), 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. We
prove that our encoding is fully abstract with
respect to barbed bisimulation and sound with
respect to barbed congruence. Our encoding
demonstrates that higher-order process-passing
together with mobile resources in, possibly local,
named locations are sufficient to express π-calculus
name-passing. The encoding uses a novel continuation
passing style to facilitate the encoding of
synchronous communication.}
}
@inproceedings{Bundgaard:08:FormalHOMBussinessProcBindBigr,
author = {Mikkel Bundgaard and Arne J. Glenstrup and
Thomas T. Hildebrandt and Espen Høsgaard and
Henning Niss},
title = {Formalizing Higher-Order Mobile Embedded Business Processes
with Binding Bigraphs},
booktitle = {Proceedings of the 10th International Conference on Coordination Models and Languages (COORDINATION'08)},
pages = {83--99},
year = 2008,
editor = {Doug Lea and Gianluigi Zavattaro},
volume = 5052,
series = {Lecture Notes in Computer Science},
publisher = {Springer Verlag},
doi = {10.1007/978-3-540-68265-3_6},
pdf = {http://itu.dk/people/mikkelbu/papers/coordination08.pdf},
abstract = {We propose and formalize HomeBPEL, a higher-order
WSBPEL-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 WSBPEL 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. We
provide a formal semantics based on binding
bigraphical reactive systems implemented in the BPL
Tool as part of the Bigraphical Programming
Languages project at ITU. The semantics is an
extension of a semantics given previously for a
simplified subset of WS-BPEL and exploits the close
correspondence between bigraphs and XML to provide a
formalized run-time format very close to standard
WS-BPEL syntax, which also constitutes the
representation of frozen sub-instances.}
}
@inproceedings{Hildebrandt:08:AdaptiveBusiProces3GERP,
author = {Thomas Hildebrandt and Arne J. Glenstrup and Mikkel Bundgaard and
Espen Højsgaard and Tim Hallwyl and Tijs Slaats and
Magnus Nilsson and Kjeld Schmidt},
title = {Computer Supported Mobile Adaptive Business Processes for 3gERP Systems},
booktitle = {2nd Workshop on 3rd Generation Enterprise Resource Planning Systems},
optpages = {},
year = 2008,
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optpublisher = {},
pdf = {},
abstract = {}
}
@inproceedings{Bundgaard:08:SeamDistMobWorkflow,
author = {Mikkel Bundgaard and Thomas Hildebrandt and Espen Højsgaard},
title = {Seamlessly Distributed and Mobile Workflow: or The right processes at the right places},
booktitle = {Proceedings of the First Workshop on Programming Language Approaches to
Concurrency and Communication-cEntric Software (PLACES'08)},
pages = {64--69},
year = 2008,
editor = {Vasco T. Vasconcelos and Nobuko Yoshida},
optvolume = {},
optnumber = {},
optseries = {},
optpublisher = {},
pdf = {http://itu.dk/people/mikkelbu/papers/places08.pdf},
abstract = {We briefly outline some of the paths being explored
within two recently initiated research projects on
Computer Supported Mobile Adaptive Business
Processes (CosmoBiz) and Trustworthy Pervasive
Healthcare Services (TrustCare) to provide flexible
process languages and models that allow seamless,
trustworthy distribution and mobility of workflows
and business process. In particular, we consider
higher-order mobile embedded business processes,
declarative versus imperative process
specifications, and communication-centric
architectures versus distributed shared storage.}
}
@inproceedings{Bundgaard:09:DecidFragOfHomer,
author = {Mikkel Bundgaard and Godskesen, Jens Chr. and Bj\o rn Haagensen and Hans H\"uttel},
title = {Decidable Fragments of a Higher Order Calculus with Locations},
booktitle = {Proceedings of the 15th International Workshop on
Expressiveness in Concurrency (EXPRESS'08)},
pages = {113--138},
year = 2009,
editor = {Thomas Hildebrandt and Daniele Gorla},
volume = 242,
number = 1,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
abstract = {Homer is a higher order process calculus with
locations. In this paper we study Homer in the
setting of the semantic finite control property,
which is a finite reachability criterion that
implies decidability of barbed bisimilarity. We show
that strong and weak barbed bisimilarity are
undecidable for Homer. We then identify and compare
two distinct subcalculi of Homer that both satisfy
the semantic finite control property. One
subcalculus is obtained by using a type system
bounding the size of process terms. The other
subcalculus is obtained by considering the image of
the encoding of the finite control pi-calculus in
Homer.}
}
@inbook{Bundgaard:10:UnfoldingCSP,
author = {Mikkel Bundgaard and Robin Milner},
editor = {Cliff B. Jones and A.W. Roscoe and Kenneth R. Wood},
title = {Reflections on the Work of C.A.R. Hoare},
chapter = {Unfolding CSP},
publisher = {Springer Verlag},
year = 2010,
series = {History of Computing},
edition = {First},
pages = {213--228},
pdf = {http://www.itu.dk/people/mikkelbu/papers/unfoldingCsp10.pdf},
abstract = {This paper demonstrates that a wide range of the CSP
operators, in particular parallel composition,
hiding, general choice, interleaving, and the
non-deterministic OR, can be represented by
confluent unfolding to a normal form. The relevant
normal form is an enrichment of the CSP choice
construction by the inclusion of non-determinism and
silent actions. It is demonstrated that the majority
of the equational laws presented by Hoare for these
operators are valid not only for the failures
equivalence but even for strong bisimilarity. This
work is a prelude to embedding CSP in the bigraph
model, a recent generic model for ubiquitous
computing in which other process calculi have been
faithfully embedded. The authors hope by this means
to elucidate the differences and similarities
between CSP and other calculi. The present paper
presents the main ideas of the embedding in the
formalism of CSP itself, and makes no use of
bigraphs in doing so.}
}
This file was generated by bibtex2html 1.96.