Abstract:
Having recalled the basics concerning lambda-mu-calculus introduced by Michel Parigot in order to extend Curry-Howard isomorphism to classical natural deduction I will present a result by Rene' David and Walter Py showing that Separation property (often refered to as Bo"hm theorem) is not satisfied in lambda-mu-calculus.

We will then consider how to recover the property by analyzing what is the reason for its failure in the original calculus. The resulting calculus, the Lambda-mu-caluclus for which Separation property holds will be compared to Parigot's calculus and with a variant introduced by Philippe de Groote. We will in particular see how Lambda-mu can be considered as a calculus of terms and streams of terms.

Purely local type checking is extended to distributed systems by associating access control lists with cryptographic keys. When a piece of data is sent outside of a type checked area it is encrypted with a key that represents the list of principles that can access that data. When encrypted data is received, the access restrictions from the decryption key are used as the access control type.

This work was carried out with Dominic Duggan and Jan Vitek.

We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n. We show that the sliding window protocol is branching bisimilar to a queue of capacity 2n. The proof is given entirely on the basis of an axiomatic theory, and was checked with the help of PVS.

(This is joint work with Bahareh Badban, Wan Fokkink , Jan Friso Groote and Jaco van de Pol.)

Abstract:
Proof Search is a updating of the logic programming paradigm where proof theory is used to motivation new designs. A great deal of work in proof theory and computation has taken place in recent years. One recent development has been the development of a good proof theory for defined predicates, which is closely related to reasoning within fixpoints and to the closed-world-assumption.

In this talk, I will illustrate some recent results in this area, present many different examples, and demonstrate a recent prototype system, Level 0/1, by Alwen Tiu. I hope to explore to what extent this work on logic and its implementation might have in doing (symbolic) model checking.

Some related paper: Some of the following paper focus on higher-order abstract syntax and the nabla; quantifier. I will not focus on these aspects of this work in this talk: instead, the focus will be on first-order logic.

Abstract:
Security protocols provide the ability of communicating privately using public means. A certain category of such protocols rely on probabilistic decisions and use primitives such as the Oblivious Transfer. Even though probabilistic protocols have been studied using model checking methods, little attempt of applying process calculi techniques has been made.

In this talk, we use a probabilistic variant of pi-calculus in order to model probabilistic protocols. We present a method of expressing some desired properties of such protocols which involves the construction of a proper specification and the introduction of a suitable precongruence relation between processes. We finally apply our method to the Partial Secrets Exchange protocol and prove its fairness.

Abstract:
In this talk, we introduce several notions of reduction in distributed computing, and investigate reduction properties of two fundamental agreement tasks, namely Consensus and Atomic Commitment.

We first propose the notion of reduction "à la Karp", an analog for distributed computing of the classical Karp reduction. We then define a weaker reduction which is the analog of Cook reduction. These two reductions are called K- reduction and C-reduction, respectively.

We establish various reducibility and irreducibility theorems with respect to these two reductions. Our main result is an incomparability statement for Consensus and Atomic Commitment tasks: we show that they are incomparable with respect to the C-reduction, except when the resiliency degree is 1, in which case Atomic Commitment is strictly harder than Consensus. A side consequence of these results is that our notion of C-reduction is strictly weaker than the one of K-reduction.

Finally, we introduce a third notion of reduction which measures the hardness to solve a task in terms of the information about failures required to solve the task. We prove that this latter reduction is strictly weaker than the C-reduction. In other words, the information about failures -- or equivalently, the weakest failure detector -- needed to solve a task does not entirely capture the hardness of the task.

Abstract:
Group communication is a topic studied since more than twenty years. During this period significant results have been obtained. Nevertheless there are issues that have not been addressed adequately. The paper presents both the important results related to group communication that have been obtained, but also points out what remains to be done to make group communication widely used, and as successful as some of the existing middleware technologies.

Abstract:
We study a process calculus which combines both nondeterministic and probabilistic behavior in the style of Segala and Lynch's probabilistic automata. We consider various strong and weak behavioral equivalences, and we provide complete axiomatizations for finite state processes, restricted to guarded definitions in case of the weak equivalences. We conjecture that in the general case of unguarded recursion the ``natural'' weak equivalences are undecidable. This is the first work, to our knowledge, that provides a complete axiomatization for weak equivalences in the presence of recursion and both nondeterministic and probabilistic choice.

Abstract:
In this talk, I'll present the use a general formal framework encoding name-passing process calculi and allowing to reason about them, using the nabla quantifier, definitions and higher-order abstract syntax. I'll show how this framework can be used to specify a format for bisimulation to be a congruence. Finally, I'll try to sketch what a model of this theory could be, and how it would connect with our applied result.

Abstract:
I will present an outline of formal and computational methods that can be used to "prove" a process secure and I will outline some the problems with these methods; this will be a basic introduction aimed at formal methods people who do not have a back ground in security. I will then describe some of the work that has been done to bridge the gap between these formal and computational worlds, which mostly consists of finding computational criteria that, when met, ensure that formal analysis and computation coincide. Finally, I will suggest a new line of work that I am undertaking, which involves extending the pi-calculus with primitives for guessing new names and a method of finding the cost of a trace that will allow analysis that approximates computational methods without the need to do any difficult computational proofs. This new work is in a very early stage and so will be largely conjecture.

Abstract:
This work compares the expressiveness of ambient calculi against different dialects of the pi-calculus. Cardelli and Gordon encoded the asynchronous pi-calculus into the ambient calculus (Mobile Ambients). Zimmer has shown that the synchronous pi-calculus without choice can be encoded in pure (no communication) Safe Ambients. We show that the pure ambient calculus without restriction has symmetric electoral systems, that is, it is possible to solve the problem of electing a leader in a symmetric network. By the work of Palamidessi, this implies that this fragment of the ambient calculus is not encodable (under certain conditions) in the pi-calculus with separate choice.

Abstract:
Finite state models prevail in today's specification and verification techniques. Global Computing systems are, however, inherently open --e.g., typically there is no bound on the number of resources/devices that can be added to a given system. So, the assumption I shall be working with is that many phenomena in Global Computing are best described in infinite-state models.

In this talk I shall give an overview of my current interests and work on infinite behavior in two areas of computer science: Concurrency Theory and Computability. Concerning the former, I shall give an overview of my work on the expressive power of different ways of specifying infinite-behaviour in process calculi. As for the latter, I shall introduce a new framework for Infinite Satisfaction Problems (basically, Infinite SAT Problems) and present some (un)decidability results we have identified for this kind of problems. These results have an impact on Open Constraint Problems; a framework recently introduced for constraint problems in Global Computing scenarios.

My work on infinite satisfaction and behaviour involves several co-authors. The following list of relevant work acknowledges all of them: