The following is a complete listing of my papers. The papers are listed in chronological order and partitioned into three categories: Conference, Journal, and Workshop Publications; Technical Reports; and Unpublished Papers.

View abstracts

Conference, Journal, and Workshop Publications

[Bundgaard and Milner, 2010]
Bundgaard, M. and Milner, R. (2010). Reflections on the Work of C.A.R. Hoare, chapter Unfolding CSP, pages 213-228. History of Computing. Springer Verlag, first edition. [ bib | .pdf ]

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.

[Bundgaard et al., 2009]
Bundgaard, M., Godskesen, J. C., rn Haagensen, B., and Hüttel, H. (2009). Decidable fragments of a higher order calculus with locations. In Hildebrandt, T. and Gorla, D., editors, Proceedings of the 15th International Workshop on Expressiveness in Concurrency (EXPRESS'08), volume 242 of Electronic Notes in Theoretical Computer Science, pages 113-138. Elsevier. [ bib ]

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.

[Bundgaard et al., 2008a]
Bundgaard, M., Glenstrup, A. J., Hildebrandt, T. T., Høsgaard, E., and Niss, H. (2008a). Formalizing higher-order mobile embedded business processes with binding bigraphs. In Lea, D. and Zavattaro, G., editors, Proceedings of the 10th International Conference on Coordination Models and Languages (COORDINATION'08), volume 5052 of Lecture Notes in Computer Science, pages 83-99. Springer Verlag. [ bib | DOI | .pdf ]

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.

[Hildebrandt et al., 2008]
Hildebrandt, T., Glenstrup, A. J., Bundgaard, M., Højsgaard, E., Hallwyl, T., Slaats, T., Nilsson, M., and Schmidt, K. (2008). Computer supported mobile adaptive business processes for 3gerp systems. In 2nd Workshop on 3rd Generation Enterprise Resource Planning Systems. [ bib | www: ]

[Bundgaard et al., 2008b]
Bundgaard, M., Hildebrandt, T., and Højsgaard, E. (2008b). Seamlessly distributed and mobile workflow: or the right processes at the right places. In Vasconcelos, V. T. and Yoshida, N., editors, Proceedings of the First Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES'08), pages 64-69. [ bib | .pdf ]

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.

[Bundgaard et al., 2007]
Bundgaard, M., Hildebrandt, T., and Godskesen, J. C. (2007). Modelling the security of smart cards by hard and soft types for higher-order mobile embedded resources. In Gorla, D. and Palamidessi, C., editors, Proceedings of the 5th International Workshop on Security Issues in Concurrency (SecCo'07), volume 194 of Electronic Notes in Theoretical Computer Science, pages 23-38. Elsevier. [ bib | DOI | .pdf ]

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.

[Bundgaard, 2007]
Bundgaard, M. (2007). Semantics of Higher-Order Mobile Embedded Resources and Local Names. PhD thesis, IT University of Copenhagen. [ bib | .pdf ]

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 π-calculus in Homer. The encoding establishes that process-passing together with mobile resources in, possibly local, named locations are sufficient to express π-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 λ-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 id. 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 π-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.

[Birkedal et al., 2006]
Birkedal, L., Bundgaard, M., Damgaard, T. C., Debois, S., Elsborg, E., Glenstrup, A. J., Hildebrandt, T., Milner, R., and Niss, H. (2006). Bigraphical programming languages for pervasive computing. In Strang, T., Cahill, V., and Quigley, A., editors, Proceedings of the 1st International Workshop on Combining Theory and Systems Building in Pervasive Computing, pages 653-658. [ bib | www: ]

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 Context-awareness, business processes and Reactive XML, axiomatisation and matching, and higher-order mobile embedded resources.

[Bundgaard and Sassone, 2006]
Bundgaard, M. and Sassone, V. (2006). Typed polyadic pi-calculus in bigraphs. In Proceedings of the 8th ACM SIGPLAN international conference on Principles and Practice of Declarative Programming (PPDP'06), pages 1-12. ACM Press. [ bib | DOI | slides | .pdf ]

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 typed polyadic π-calculus with capability types à la Pierce and Sangiorgi, which we represent using a novel kind of link sorting called subsorting. Using the theory of 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) π-calculus as sortings in the setting of bigraphs.

[Bundgaard and Hildebrandt, 2006]
Bundgaard, M. and Hildebrandt, T. (2006). Bigraphical semantics of higher-order mobile embedded resources with local names. In Rensink, A., Heckel, R., and König, B., editors, Proceedings of the Graph Transformation for Verification and Concurrency workshop (GT-VC'05), volume 154 of Electronic Notes in Theoretical Computer Science, pages 7-29. Elsevier. [ bib | DOI | slides | .pdf ]

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 π-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 Higher-Order Mobile Embedded Resources (Homer). The presentation is based on Milner's recent presentation of the λ-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 localised bigraphs as a generalisation of local bigraphs in which links can be further localised.

[Bundgaard et al., 2006]
Bundgaard, M., Hildebrandt, T., and Godskesen, J. C. (2006). A CPS encoding of name-passing in higher-order mobile embedded resources. Theoretical Computer Science, 356(3):422-439. [ bib | DOI | .pdf ]

We present an encoding of the synchronous π-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.

[Bundgaard et al., 2005]
Bundgaard, M., Hildebrandt, T., and Godskesen, J. C. (2005). A CPS encoding of name-passing in higher-order mobile embedded resources. In Baeten, J. and Corradini, F., editors, Proceedings of the 11th International Workshop on Expressiveness in Concurrency (EXPRESS'04), volume 128 of Electronic Notes in Theoretical Computer Science, pages 131-150. Elsevier. [ bib | DOI | slides | .pdf ]

We present an encoding of the synchronous π-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 π-calculus name-passing. The encoding uses a novel continuation passing style to facilitate the encoding of synchronous communication.

Technical Reports

[Birkedal et al., 2009]
Birkedal, L., Bundgaard, M., Debois, S., Grohmann, D., and Hildebrandt, T. (2009). Higher-order contexts via games and the Int-construction. Technical Report TR-2009-117, IT University of Copenhagen. [ bib | .pdf ]

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.

[Bundgaard et al., 2008b]
Bundgaard, M., Godskesen, J. C., and Hildebrandt, T. (2008b). On encoding the π-calculus in higher-order calculi. Technical Report TR-2008-106, IT University of Copenhagen. [ bib | .pdf ]

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 π-calculus in higher-order calculi: the encoding in HOπ-calculus by Sangiorgi and Walker and the encoding in Plain CHOCS by Thomsen. We propose a new encoding of the synchronous π-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 π-calculus name-passing.

[Bundgaard et al., 2008a]
Bundgaard, M., Glenstrup, A. J., Hildebrandt, T., Højsgaard, E., and Niss, H. (2008a). Formalizing WS-BPEL and higher order mobile embedded business processes in the bigraphical programming languages (BPL) Tool. Technical Report TR-2008-106, IT University of Copenhagen. [ bib | .pdf ]

Bigraphical Reactive Systems (BRSs) have been proposed as a formal meta-model for global ubiquitous computing that encompasses process calculi for mobility, notably the π-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.

[Bundgaard et al., 2007]
Bundgaard, M., Hildebrandt, T., and Godskesen, J. C. (2007). Typing linear and non-linear higher-order mobile embedded resources with local names. Technical Report TR-2007-97, IT University of Copenhagen. [ bib | .pdf ]

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.

[Bundgaard and Hildebrandt, 2005]
Bundgaard, M. and Hildebrandt, T. (2005). Bigraphical semantics of higher-order mobile embedded resources with local names. Technical Report TR-2005-70, IT University of Copenhagen. [ bib | .pdf ]

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 π-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 Higher-Order Mobile Embedded Resources (Homer). The presentation is based on Milner's recent presentation of the λ-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 localised bigraphs as a generalisation of local bigraphs in which links can be further localised.

[Hildebrandt et al., 2004]
Hildebrandt, T., Godskesen, J. C., and Bundgaard, M. (2004). Bisimulation congruences for Homer - a calculus of higher order mobile embedded resources. Technical Report TR-2004-52, IT University of Copenhagen. [ bib | .pdf ]

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.

Non-peer Reviewed and Unpublished Papers, and Drafts

[Bundgaard et al., 2009]
Bundgaard, M., Godskesen, J. C., rn Haagensen, B., and Hüttel, H. (2009). Decidable fragments of a higher order calculus with locations. Long version of [?]. Submitted for publication. [ bib ]
[Hildebrandt et al., 2007]
Hildebrandt, T., Niss, H., Bundgaard, M., Schmidt, K., and Jensen, T. (2007). Computer supported mobile adaptive business processes: Position paper on the cosmobiz research project (2007-2010). In Proceedings of 1st Informal Workshop on Formal Models and Notations for Business Process Execution, Service Oriented Computing and CSCW". [ bib | .pdf ]

Dynamic evolution of workflow process descriptions and active instances has been an active research area since the mid 1990s. Most work has been based on flow-graph meta models formalised as variations of Petri Nets. We present a new research project on Computer Supported Mobile Adaptive Business Processes (CosmoBiz) initiated in January 2007 jointly with Microsoft Development Center Copenhagen, which will extend this work to mobile and distributed workflows, by uniting research in formal models for graph rewriting and typed process calculi, design and implementation of distributed and peer-to-peer systems, and computer supported collaborative work.

[Bundgaard, 2006]
Bundgaard, M. (2006). Handin for the PhD course a derivational approach to calculi, evaluation, and abstract machines. [ bib | .pdf ]

In this report we examine the transformation of an big-step relation, for finding matches in place graphs, into a small-step transition relation which solves the same task.

[Bundgaard, 2004]
Bundgaard, M. (2004). Introduction to the mobility workbench. Part of the curriculum for the course Modelbased design of distributed and mobile systems. [ bib ]

This file was generated by bibtex2html 1.96.

Note: Just updated the homepage. Wait for more information :)

Subpages