Abstracts

In my talk I will give a gentle introduction to the CLF type theory and demo the type inference and logic programming features of the Celf system.

A similar issue was already raised in linear logic, leading to the definition of a certain category of focalised executions. Such executions constraints the evaluation of the two programs so that all the executions of the first one are done before it starts to execute the transitions of the second. It is then proved, in linear logic, that the proof search is not weakened, while the complexity of the search is greatly reduced.

The work presented here propose a transposition of this technique to the asynchronous pi-calculus. Hence, we define the notion of focalised transitions for the asynchronous pi-calculus, allowing to greatly reduce the complixity of the evaluation of a process. Furthermore, we prove that we preserve all the available information on the processes while using focalised transitions.

To deal with proof identity, we need new proof systems with a much improved ability to see the fine detail of proofs, i.e., we need systems whose inference rules only deal with a minimal amount of information. These rules are called `local' and cannot be obtained in the traditional proof theory. However, locality is achievable by adopting a relatively novel approach to the structure of proofs, that we call `deep inference'. Thanks to locality, not only are we able to see more detail, we are also able to discard unnecessary detail, the so-called `bureaucracy' of traditional proof systems. In particular, we can show that normalisation can be achieved in a largely syntax-independent way by removing bureaucracy from deep-inference proofs, and reducing them to their `atomic flow'.

We are about to satisfactorily solve the proof identity problem, by a coordinated effort involving several research groups. We have also made progress towards reducing the complexity of proofs and of their normalisation.

I will give an accessible survey of these topics, for anybody with an interest in the theoretical foundations of computer science. More on deep inference at http://alessio.guglielmi.name/res/cos.

However, cut-elimination is an inherently non-deterministic process. At each stage one has the choice between different cuts to reduce and - for a single cut - there are different ways of reducing it. It is not clear, in how far this formal non-determinism may lead to mathematical differences in the resulting elementary proofs. Understanding the possible span of the results of cut-elimination procedures is of fundamental importance for judging proof analyses based on these methods.

In this talk I will treat the standard syntactic cut-elimination for first-order classical logic and report on a recent result obtained jointly with M. Baaz on the non-confluence of this reduction: It is possible to construct a sequence of polynomial-size proofs s.t. a proof in this sequence has non-elementarily many different cut-free normal forms (each of non-elementary size). These normal forms are different in a strong sense: They not only represent different Herbrand-disjunctions but also have different propositional structures and hence are not substitution-instances of a single general proof.

This result shows that the constructive content of a cut-free proof does not only depend on the proof with cuts from which it was generated but also on the way the cuts are eliminated.

(The talk is based on joint work with Rob van Glabbeek, Matthew Hennessy, Carroll Morgan, and Chenyi Zhang)

If time permits, I will discuss two additional results:

(i) a sound and complete axiomatization of bisimilarity, and

(ii) the proof that bisimilarity becomes undecidable if at least four static (i.e., top-level) restrictions are added to the calculus.

Keywords: modal logic (conditional, epistemic, provability, and temporal), knowledge (individual, propositional, common, and adductive), designated-verifier proofs, multi-agent systems

Keywords:

malware (computer viruses, worms, Trojan horses, etc.), benware, anti-malware, medware, modal logic, formal software engineering

The encoding of the lambda-calculus uses instead a polyadic constraint system but it is compositional unlike that of Minsky machines. Compositionality is an important property of an encoding as it may allow structural analysis in utcc of the source terms; i.e., functional programs.

In summary, we show the full computational expressiveness of utcc, its compositional correspondence to functional programming (lambda-calculus), and its applicability for proving new results in standard concurrency formalisms such as FLTL.

[4] N. Busi, M. Gabbrielli, and G. Zavattaro. Comparing recursion, replication, and iteration in process calculi. In ICALP'04, volume 3142 of Lecture Notes in Computer Science, pages 307-319. Springer-Verlag, 2004.

Our extended system enjoys the analytical theorems of ludics in a suitably modified form. In addition, we prove a general form of full completeness with respect to coinductively defined behaviours and infinitary proofs.

Finally, an analysis is made on those designs representing data objects. We show that any set of finite data forms a behaviour, and then discuss acceptance of languages via normalization.<>

(i) the best known encodings appeared in the literature satisfy them;

(ii) this notion is not trivial, because there exist encodings that do not satisfy all the criteria we have proposed;

(iii) the best known separation results can be formulated in terms of our criteria; and

(iv) some widely believed (but never proved) separation results can be proved by using the criteria we propose.

Moreover, the way in which we prove known separation results is easier than the way in which such results were originally proved.

A domain-theoretic denotational semantic has been defined in [2] that maps a process to the supremum store that it can reach. It is then possible to compute this supremum store by a fixed point construction, based on the grammar of the process.

This article studies an extension of concurrent constraint programming with probabilistic executions. Although similar kinds of extensions have already been investigated in the literature[3, 4] , we are interested in extending the original operational and denotational semantics in the most natural way. To do this, we propose to model the probabilistic CCP as a probabilistic powerdomain, similar to the one described int [5], built on top of the original constraint lattice.

We apply those result to a very simple probabilistic CCP based on the original CCP, with blind probabilistic choice added. Results show a very natural extension of the original denotational semantic.

References:

[1]: Concurrent Constraint Programming Languages, Vijay A. Saraswat, PhD Thesis, Carnegie-Melon University, 1989

[2]: Semantic Foundations of Concurrent Constraint Programming, Vijay A. Saraswat and Martin Rinard and Prakash Panangaden, Conference Record of the Eighteenth Annual {ACM} Symposium on Principles of Programming Languages, 1991

[3]: Probabilistic Concurrent Constraint Programming, Vineet Gupta and Radha Jagadeesan and Vijay A. Saraswat, International Conference on Concurrency Theory, 1997

[4]: Stochastic Processes as Concurrent Constraint Programs, Vineet Gupta and Radha Jagadeesan and Prakash Panangaden, Symposium on Principles of Programming Languages, 1999

[5]: The troublesome probabilistic powerdomain, A. Jung and R. Tix, Third Workshop on Computation and Approximation, 1998