@INPROCEEDINGS{Bidinger:TCS08,
author = {Philippe Bidinger and Adriana Compagnoni},
title = {Pict Correctness Revisited},
year = {2008},
url = {./pict_tcs2008.pdf},
abstract = {
The Pict programming language is an implementation of the pi-calculus in which executions
of pi-calculus terms are specified via an abstract machine.An important property of any concurrent programming language
implementation is the
fair execution of threads. After defining fairness for the pi-calculus, we show
that Pict abstract machine executions implement fair pi-calculus executions.
We also give new proofs of soundness and liveness for the Pict abstract machine.
},
note = {Submitted to Theoretical Computer Science. Coordination/FMOODS'07 Special
Issue. This paper subsumes \cite{Bidinger:FMOODS07}}
}
@INPROCEEDINGS{Compagnoni:TCS08,
author = {Adriana Compagnoni and Elsa L. Gunter and Philippe Bidinger},
title = {Role-Based Access Control for Boxed Ambients},
year = {2008},
booktitle = {Theoretical Computer Science. Festschrift in Honor of Mariangiola Dezani-Ciancaglini, Simona Ronchi Della Rocca},
series = {Lecture Notes in Computer Science},
abstract = {
In this paper we describe a calculus for mobile processes and
propose a mechanism for specifying access
privileges based on a combination of the identity of the users
seeking access, their credentials, and the location from which they
seek it, within a reconfigurable nested structure.},
note = {To appear}
}
@INPROCEEDINGS{Basu:FORTE2008,
author = {Ananda Basu and Philippe Bidinger and Marius Bozga and Joseph Sifakis},
title = {Distributed Semantics and Implementation for Systems with Interaction and Priority},
booktitle = {Formal Techniques for Networked and Distributed Systems
- FORTE 2008, 28th IFIP WG 6.1 International Conference,
Tokyo, Japan, June 10-13, 2008, Proceedings},
series = {Lecture Notes in Computer Science},
year = 2008,
month = JUNE,
url = {./forte2008.pdf},
abstract = {
The paper studies a distributed implementation method for the BIP
(Behavior, Interaction, Priority) component framework for modeling
heterogeneous systems.
}
}
@INPROCEEDINGS{Bidinger:FMOODS07,
author = {Philippe Bidinger and
Adriana B. Compagnoni},
title = {Pict Correctness Revisited},
year = {2007},
pages = {206-220},
editor = {Marcello M. Bonsangue and
Einar Broch Johnsen},
booktitle = {Formal Methods for Open Object-Based Distributed Systems,
9th IFIP WG 6.1 International Conference, FMOODS 2007, Paphos,
Cyprus, June 6-8, 2007, Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4468},
isbn = {978-3-540-72919-8},
url = {./fmoods2007.pdf}
}
@INPROCEEDINGS{Bidinger:SAVCBS05,
author = {Philippe Bidinger and Matthieu Leclercq and Vivien Qu\'ema and Alan Schmitt and Jean-Bernard Stefani},
title = {{Dream Types - A Domain Specific Type System for Component-Based Message-Oriented Middleware}},
booktitle = {4th Workshop on Specification and Verification of Component-Based Systems (SAVCBS'05), in association with ESEC/FSE'05},
address = {Lisbon, Portugal},
month = SEPTEMBER,
year = 2005,
url = {./savcbs2005.pdf},
abstract = {
We present a type system for the dream component-based message-oriented
middleware. This type system aims at preventing the erroneous use of
messages, such as the access of missing content. To this end, we adapt to
our setting a type system developed for extensible records.
}
}
@INPROCEEDINGS{Bidinger:FMOODS05,
title = {An Abstract Machine for the {K}ell Calculus},
author = {Philippe Bidinger and Alan Schmitt and Jean-Bernard Stefani},
year = 2005,
month = JUN,
booktitle = {Formal Methods for Open Object-Based Distributed Systems,
7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens,
Greece, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3535},
pages = {43--58},
note = {Best Paper Award},
address = {Athens, Greece},
url = {./fmoods2005.pdf},
abstract = {
The Kell Calculus is a family of process calculi intended as a
basis for studying distributed component-based programming. This
paper presents an abstract machine for an instance of this calculus,
a proof of its correctness, and a prototype OCaml implementation.
The main originality of our abstract machine is that it does not
mandate a particular physical configuration (e.g.\ mapping of
localities to physical sites), and it is independent of any
supporting network services. This allows to separate the proof of
correctness of the abstract machine per se, from the proof of
correctness of higher-level communication and migration protocols
which can be implemented on the machine.
}
}
@INPROCEEDINGS{Bidinger:FMOODS03,
author = {P. Bidinger and J.B. Stefani},
title = {{The Kell Calculus: Operational Semantics and Type System}},
booktitle = {Formal Methods for Open Object-Based Distributed Systems,
6th IFIP WG 6.1 International Conference, FMOODS 2003, Paris,
France, 2005, Proceedings},
volume = {2884},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
year = {2003},
url = {./fmoods2003.pdf},
abstract = {
This paper
presents the Kell calculus, a new distributed
process calculus that retains the original insights of the Seal
calculus (local actions, process replication) and of the M-calculus
(higher-order processes and programmable membranes), although in
a much simpler setting than the latter. The calculus is equipped with
a type system that enforces a unicity property for location names that
is crucial for the efficient implementation of the calculus.
}
}
This file has been generated by bibtex2html 1.85.