Home People Papers & Software Seminar Stages
 Comète-Parsifal Seminar (Abstracts 2006)

## Calendar

2012 2011 2010 2009 2008 2007 2006 2005 2004
 2006 Fri Dec 15, 14:00 Sergio Maffeis Computational strength and expressivity results for process calculi using encodings. Tue Dec 12, 14:00 Alexis Saurin Focalization as proof normalization Tue Dec 5, 14:00 Martin Hutle Searching the Weakest Model for Consensus Mon Dec 4, 11:00 Pietro Abate The Tableau WorkBench Nov 24, 14:00 Romain Beauxis On the Asynchronous Nature of the Asynchronous Pi Calculus Nov 23, 14:00 Pierre Sutra Eventual consistency and commitment in semantically-rich distributed systems Nov 21, 14:00 Giulio Manzonetto R.e. Theories versus Effective Models Oct 31 Kostas Chatzikokolakis and Catuscia Palamidessi Anonymity Protocols as Noisy Channels Oct 25 Frank Valencia On Linearity vs Persistence and a FOL Interpretation of the pi-calculus Oct 20 Glynn Winskel Event structures with symmetry Oct 17 Chuck Liang Aspect-Oriented Programming in Higher-Order and Linear Logic Sep 26 Tom Chothia Analysing the MUTE Anonymous File-Sharing System Using the Pi-calculus Jun 23 John Mullins Analyse de flux d'information dans les protocoles cryptographique Jun 15 Bernadette Charron-Bost The Iconoclast Hear-Of Model: Unifying all Benign Failures Jun 13 Francois Lamarche Sémantique dénotationelle des preuves en logique classique May 12 Cinzia Di Giusto The Power of Divergency May 11 Sebastien Briais Open Bisimulation, Revisited May 9 Steve Kremer Coercion-Resistance and Receipt-Freeness in Electronic Voting Apr 4 Sylvain Peyronnet Approximate probabilistic verification Mar 31 Patrick Thévenon The DemoNat project Mar 7 Daniele Gorla Comparing Communication Primitives via their Relative Expressive Power Jan 10 Gopalan Nadathur Practical Higher-Order Pattern Unification with On-the-Fly Raising

## Abstracts

Dec 15 2006, 14:00
Speaker: Sergio Maffeis
Title: Computational strength and expressivity results for process calculi using encodings.

Abstract:
We present an analysis of the computational strength of sub-languages of the Ambient Calculus, and a study of the expressive power of polyadic synchronization in pi-calculus to illustrate the use of encodings as a means of comparison between languages. In particular, in the Ambient calculus, we show that the presence of movement capabilities marks the boundary between Turing equivalence and termination. In the pi-calculus, we show that polyadic synchronization, which gives the power to encode cryptography and distributed locations, cannot be encoded under some reasonably weak assumptions, without introducing the possibility of divergence.
Top

Dec 12 2006, 14:00
Speaker: Alexis Saurin
Title: Focalization as proof normalization

Abstract:
Since the introduction of focalization by Andreoli in 1992, this fundamental property of linear logic proof systems has been widely used in the linear logic community, being at the heart of works on linear logic programming, of the introduction of polarities (like in polorized linear logic) or being an essential piece in the recent ludics. However, focalization is usually considered from the completeness point of view (if there exists a proof, there exists a focussed proof) rather than from the proof transformation point of view (form any linear logic proof I can get a focussed proof). In this talk we take seriously this idea of proof transformation in order to give a proof of focalization for linear logic that uses proof tranformation techniques. Among the advantages of this approach is to stay inside standard linear logic system (and thus to view a focussed proof as a proof verifying certain constraints rather than as a proof in a different proof system which includes focalization) and to allow for a modular study of focalization and for "different degrees" of focalization (in particular for the question of the treatment of the atoms for instance) We will first study the simpler case of MALL and then draw some comments on the extension to full linear logic with cuts. We will then outline some considerations on the relationships between cut reduction and focalization.
Top

Dec 05 2006, 14:00
Speaker: Martin Hutle
Title: Searching the Weakest Model for Consensus

Abstract:
The consensus problem is one of the key problems in fault-tolerant distributed computing, and in the heart of the replication paradigm. In order to maximize the reliablity of an implementation in a real system, a consensus algorithm should rely only on a minimum of assumptions about faults and synchrony. For the latter, it is well known that consensus is solveable in a synchronous system, whereas it is impossible to solve it in a completely asynchronous system, i.e. a system without bounds on the relative processing speeds of processes and the communication delay between them. Exploring the models that lay between asynchrony and synchrony, but still allow solving consensus, has thus been a great challenge in the last two decades. Most of the more recent work was done in terms of the failure detector abstraction.

This talk reviews previous models for implementing failure detectors for consensus and presents a new model that is weaker than all previously proposed models. Then the limitations of the failure detector approach are discussed, and a new abstraction that overcomes these limitations is presented, together with some first results. An outlook for open challanges in this context concludes the talk.

Top

Dec 04 2006, 11:00
Speaker: Pietro Abate
Title: The Tableau WorkBench

Abstract:
Theorem provers have now matured dramatically. On one hand, highly optimized and specific theorem provers like Fact or MSPASS, can test formulae with hundreds of symbols within a few seconds while provers like the LWB implement many different logics in a single framework. On the other hand, theorem provers like Isabelle implement generic logical frameworks that are mainly tailored to interactive reasoning. Despite the great effort made to design intuitive user interfaces, researchers that are merely interested in mechanizing their favourite logic often find these tools too complex to modify or to program. The Tableaux WorkBench (TWB) is a generic framework for building automated theorem provers for arbitrary logics without learning complex programming languages. The TWB consists of a small core that defines its general architecture, some extra the machinery required to specify tableau-based theorem provers and an abstraction language for expressing new tableau rules. New logic modules are defined via the user interface and then translated and compiled with the proof engine to produce a specialized theorem prover for that logic. During this talk I'll present an overview of the architecture of the TWB, explain in details the tableau based specification language and I'll conclude by giving few examples including a novel one pass decision procedure for the unified branching temporal logic UB.
Top

Friday Nov 24 2006, 14:00
Speaker: Romain Beauxis
Title: On the Asynchronous Nature of the Asynchronous Pi Calculus
Abstract:
We address the question of what kind of asynchronous communication is exactly modeled by the asynchronous $\pi$-calculus ($\pi_a$). To this purpose we define a calculus $\pi_\mathfrak{B}$ where channels are represented explicitly as special buffer processes. The base language for $\pi_\mathfrak{B}$ is the (synchronous) $\pi$-calculus, except that ordinary processes communicate only via the buffers. Then we compare this calculus with $\pi_a$. It turns out that there is a strong correspondence between $\pi_a$ and $\pi_\mathfrak{B}$ in the case that buffers are bags: we can indeed encode each $\pi_a$ process into a strongly asynchronous bisimilar $\pi_\mathfrak{B}$ process, and each $\pi_\mathfrak{B}$ process into a weakly asynchronous bisimilar $\pi_a$ process. In case the buffers are queues or stacks, on the contrary, the correspondence does not hold. We show indeed that it is not possible to translate a stack or a queue into a weakly asynchronous bisimilar $\pi_a$ process. Actually, for stacks we show an even stronger result, namely that they cannot be encoded into weakly asynchronous bisimilar processes in a $\pi$-calculus without mixed choice.
Top

Thursday Nov 23 2006, 14:00
Speaker: Pierre Sutra
Title: Eventual consistency and commitment in semantically-rich distributed systems
Abstract:
Coordinating distributed systems for replication purposes or to allow collaborative work on shared data is a performance and availability bottleneck. The optimistic replication (OR) advocates the idea to decouple data access form network access. It allows processes to use a local replica without a priori synchronization. Local execution is tentative and actions may roll back later. An OR system propagates updates lazily, and ensures consistency by a global a posteriori agreement on the set and order of actions called commitment or reconciliation phase. At this point two approaches are used to deal with this reconciliation phase : a first one based on the temporality of events in the distributed system called state machine replication, and a second one based on the semantics linking tentative actions.

In this talk we will present a formal framework to reason upon optimistic replication using the semantics of distributed applications, and an algorithm to ensure the reconciliation process.
Top

Tuesday Oct 31, 2006, 14:00
Speaker: Giulio Manzonetto
Title: R.e. Theories versus Effective Models
Abstract:
In this seminar we show how syntactical and semantic properties of the programming languages can proved by topological methods. The main tool of this approach is a topology introduced by Visser in eighties in an orthogonal way with respect to the Scott topology.

In this way we can also investigate weather there exists, inside the known semantics, a model of lambda calculus whose equational theory is recursively enumerable.

We give a negative answer for the stable semantics of Berry and Girard and the strongly stable semantics of Ehrhard. We also give a partial negative result for Scott continuous semantics.
Top

Tuesday Oct 31, 2006, 14:00
Speaker: Kostas Chatzikokolakis and Catuscia Palamidessi
Title: Anonymity Protocols as Noisy Channels

Abstract:
1st Speaker: Kostas Chatzikokolakis (30 min)
We will make a brief introduction to the problem of anonymity and present some protocols designed to provide this property. Then we will discuss a probabilistic framework in which anonymity protocols are interpreted as particular kinds of channels, and the degree of anonymity provided by the protocol as the converse of the channel's capacity. We will then illustrate how various notions of anonymity can be expressed in this framework, and show the relation with probabilistic definitions of anonymity in literature.

2nd Speaker: Catuscia Palamidessi (30 min):
We will show a way to construct the matrix of the channel corresponding to an anonymity protocol by using model-checking techniques, and how to compute the capacity in some particular cases. We will illustrate this methodology on the well-known protocol of the Dining Cryptographers. Then we will show how the channel matrix associated to an anonymity protocol can be used by an adversary to try to infer the identity of the culprit from the observables, using the well-known techniques of Bayesian inference. Then we will discuss how the success of this technique, measured in terms of the Bayesian probability of error, depends critically on certain properties of the matrix.
Top

Friday Oct 20, 2006, 14:00
Speaker: Glynn Winskel
Title: Event structures with symmetry

Abstract:
I'll motivate the introduction of symmetry to event structures and sketch applications: to non-deterministic dataflow; the unfolding of Petri nets; the semantics of higher-order processes; equivalences.
Top

Tuesday Oct 17, 2006, 14:00
Speaker: Chuck Liang
Title: Aspect-Oriented Programming in Higher-Order and Linear Logic

Abstract:
"Aspect-oriented programming" is emerging as an important paradigm forsoftware development. Its attraction lies in a new approach tomodularity in the structuring of programs. In this talk I will explorethis topic from the perspective of logic programming and proof search.Extensions of Horn Clause Prolog provide richer abstraction andcontrol mechanisms. Definite clauses that pertain to a common aspect,and which "crosscut" other program components, can be encapsulatedusing the connectives of higher-order intuitionistic logic. Theintegration or "weaving" of program fragments can be formulated usingnormalized forms of proof search in linear logic. For the audience,some background in logic programming and proof search would be helpfulbut no familiarity with aspect oriented programming is required.
Top

Wednesday Oct 25 2006, 15:00
Speaker: Frank Valencia
Title: On Linearity vs Persistence and a FOL Interpretation of the pi-calculus

Abstract:
We shall present an expressiveness study of linearity and persistence of processes. We choose the pi-calculus, one of the main representatives of process calculi, as a framework to conduct our study. We consider four fragments of the pi-calculus. Each one singles out a natural source of linearity/persistence also present in other frameworks such as Concurrent Constraint Programming (CCP), Linear CCP, and several calculi for security. The study is presented by providing (or proving the non-existence of) encodings among the fragments, a processes-as-formulae interpretation and a reduction from Minsky machines. The fragments are: (1) The (polyadic) asynchronous pi-calculus Api, (2) persistent-input Api defined as Api with all inputs replicated, (3) persistent-output Api defined as Api with all outputs replicated, and (4) persistent Api defined as Api with all inputs and outputs replicated. We provide compositional fully-abstract encodings, homomorphic w.r.t the parallel operator, from (1) into (2) and (3) capturing the behaviour of source processes. In contrast, we show that it is impossible to provide such encodings from (1) into (4). Nevertheless we prove that (4) is Turing-powerful. We further show that barbed congruence is undecidable for the zero-adic version of (2), the monadic version of (3) and the bi-adic version of (4). In contrast, we also show that it is decidable for the zero-adic versions of (3) and (4).

Furthermore, we provide a compositional interpretation of the pi processes in (4) as First-Order Logic (FOL) formulae. The interpretation translates restriction and input binders into existential and universal quantifiers respectively. We illustrate how the interpretation simulates name extrusion (mobility) in FOL. We use the interpretation to characterize the standard pi-calculus notion of barbed observability (reachability) as FOL entailment. We apply this characterization and classic FOL results by Bernays, Schonfinkel and Godel to identify decidable classes (w.r.t. barbed reachability) of infinite-state processes exhibiting meaningful mobile behaviour.
Top

Jan 10, 2006
Title: Practical Higher-Order Pattern Unification with On-the-Fly Raising

Abstract:
Higher-order pattern unification problems arise often in computations within metalanguages and logical frameworks. An important characteristic of such problems is that they are given by equations appearing under a prefix of alternating universal and existential quantifiers. Most existing algorithms for solving these problems assume that such prefixes are simplified to a "forall-some-forall" form by an a priori application of a transformation known as raising. There are drawbacks to this approach. Mixed quantifier prefixes typically manifest themselves in the course of computation, thereby requiring a dynamic form of preprocessing that is difficult to support in low-level implementations. Moreover, raising may be redundant in many cases and its effect may have to be undone by a subsequent pruning transformation. An explicit substitution based method has been proposed by Dowek, Hardin, and Pfenning (DHKP) that appears to use a different technique for handling variable dependencies but the resulting algorithm nevertheless appears to give rise to a behaviour akin to undirected dynamic raising followed by pruning. We describe a method that overcomes these drawbacks. In particular, we present a unification algorithm that proceeds by recursively descending through the structures of terms, performing raising and other transformations on-the-fly and only as needed. This algorithm does not reflect explicit substitutions directly into the unification process and it treats raising in a controlled way but it still has intriguing similarities to the processing manifest in the DHKP procedure. In this talk, we will present the essential ideas underlying the new higher-order pattern unification procedure and will also discuss the relevance of explicit substitution based approaches to this particular unification problem. [This talk is based on joint work with Natalie Linnell]
Top

March 7, 2006
Speaker: Daniele Gorla
Title: Comparing Communication Primitives via their Relative Expressive Power

Abstract:
In this talk, we assess the expressiveness of 16 communication primitives, arising from the combination of four features: synchrony, arity (monadic vs polyadic data), communication medium (message passing vs shared dataspaces) and pattern-matching. Some primitives have been already used in languages appeared in literature; other ones are completely new. Thus, to uniformly reason on such primitives, we plugged them in a common framework inspired by the pi-calculus. By means of possibility/impossibility of `reasonable' encodings, we compare every pair of primitives to obtain a hierarchy of languages based on their relative expressive power.

URL: This talk partially describes a paper that will appear in FoSSaCS 06. Interested people can download it at http://www.dsi.uniroma1.it/~gorla/abstracts/FoSSaCS06.htm
Top

March 24, 2006
Speaker: Jean Krivine
Title: Fast Forward Distribution

Abstract:
Backtracking programs are common place in transactional systems where different components need to acquire a resource simultaneously (like processes trying to modify a distributed database). Despite possible temporary failures one has to ensure the correctness of the overall execution of the transaction (ie. bisimilarity with the spec in Milner's sense). The price to pay for having a correct code is one must treat explicitly the cases where the consensus could not be met. In particular, this means that programs must contain additional states necessary to undo transactions that are doomed to fail. This results in a larger state space and a possible infinite behavior of processes. In many cases this also means to abandon the hope to prove bisimulation automatically. We present a methodology, that we call Fast Forward Distribution, to derive correct distributed systems. It reduces correction to a weaker notion of causal or forward correctness by adding implicit backtracking that is already proved correct. We will see how the weak correctness condition can be proved for CCS processes, using an event structure based algorithm we have implemented in an Ocaml library.

References: (http://pauillac.inria.fr/~krivine )
V. Danos and J. Krivine "Reversible Communicating Systems."
V. Danos and J. Krivine "Transactions with RCCS."
Tool: Causal Ocaml library (http://pauillac.inria.fr/~krivine/causal/causal.html )
Top

March 31, 2006
Speaker: Patrick Thévenon
Title: The DemoNat project

Abstract:
The aim of the DemoNat project is to analyse and validate proofs in natural language. Some ideas have been developped since the beginning in September 2003. I will give an overview on the system. I will then talk more precisely about my implication in the project. My participation was in three parts. I had to : - Define a restricted language for proofs that is intermediate between natural language and formal proof. This language describes logical rules that must be validated. - Implement a prover whose aim is to validate the rules coming from the restricted language. It is mainly a resolution prover using some ideas such as lazy decomposition. - prove some theoretical things on a framework introduced by Phillipe de Groote, the abstract categorial grammars (ACG). They are a tool that can be used to make translation between structures, and could be useful in the process of translating natural language into the restricted language. The ACGs are based on a lambda calculus. Here I studied a lambda calculus with two arrows for which the notion of principal types is not so easy because of the presence of unspecified arrows.
Top

April 4, 2006
Speaker: Sylvain Peyronnet
Title: Approximate probabilistic verification

Abstract:
We study the existence of efficient approximation methods to verify quantitative specifications of probabilistic systems. Models of such systems are labelled discrete time Markov chains and checking specifications consists of computing satisfaction probabilities of linear temporal logic formulas. We show how some simple randomized approximation algorithms can improve the efficiency of verification of such probabilistic specifications.
Top

May 9, 2006, 14:00
Speaker: Steve Kremer
Title: Coercion-Resistance and Receipt-Freeness in Electronic Voting

Abstract:
We formally study important properties of electronic voting protocols. In particular we are interested in coercion-resistance and receipt-freeness. Intuitively, an election protocol is coercion-resistant if a voter A cannot prove to a potential coercer C that she voted in a particular way. We assume that $A$ cooperates with C in an interactive fashion. Receipt-freeness is a weaker property, for which we assume that A and C cannot interact during the protocol: to break receipt-freeness, A later provides evidence (the receipt) of how she voted. While receipt-freeness can be expressed using observational equivalence from the applied pi calculus, we need to introduce a new relation to capture coercion-resistance. Our formalization of coercion-resistance and receipt-freeness are quite different. Nevertheless, we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies privacy, the basic anonymity property of voting protocols, as defined in previous work. Finally we illustrate the definitions on a simplified version of the Lee et al. voting protocol.
Top

May 11, 2006, 11:00
Speaker: Sebastien Briais
Title: Open Bisimulation, Revisited

Abstract:
In the context of the pi-calculus, open bisimulation is prominent and popular due to its congruence properties and its easy implementability. Motivated by the attempt to generalise it to the spi-calculus, we offer a new, more refined definition and show in how far it coincides with the original one. We then show its generalisation to the spi-calculus.
Top

May 12, 2006, 15:00
Speaker: Cinzia Di Giusto
Title: The Power of Divergency

Abstract:
Different tecniques can be adopted to compare concurrent languages, one of these methods focuses on computability: showing that some important properties such as termination, convergence, etc, are decidable in one language but not in the other. I will present some known results on the comparision between replication and recursion in CCS. Starting from this results I will give you some insights on the meaning of divergency in those calculi by discussing some conjectures on its strong impact on expressiveness. In particular I conjecture that disallowing divergency renders an otherwise Turing-Powerful formalism into a one which sits below CFL in the Chomsky Hierarchy.
Top

June 13, 2006, 14:00
Speaker: Francois Lamarche
Title: Sémantique dénotationelle des preuves en logique classique.

Abstract:
La logique linéaire est parfaitment symétrique : la négationest involutive, etelle échange la conjonction (tenseur) et la disjonction (par). Elle est née dela remarque, faite par Girard, que la catégorie des espaces cohérents et desfonctions stables possédait ces symmétries : un système déductif a été inventépour saisir ces propriétés.
La logique classique a les memes propriétés de symétrie au niveau de laprouvabilité, mais jusqu'à maintenant on ne connaissait pas de sémantique despreuves où ces symétries étaient conservées. Nous allons présenter desvariations sur le thème des espaces cohérents qui permettent d'avoir dessémantiques "parfaites" de la logique classique, et énoncer certainesconditions abstraites qui sont nécessaires pour que ça fonctionne. Le conceptd'espacé cohérent doit etre généralisé dans deux directions, dont une estnouvelle et l'autre a été présentée par l'auteur à MFPS 1995.
Top

June 15, 2006, 14:00
Title: The Iconoclast Hear-Of Model: Unifying all Benign Failures

Abstract:
Problems in fault-tolerant distributed computing have been studied ina variety ofmodels. These models are structured around two central dogmas:
1. Degree of synchrony and failure model are two independentparameters that determinea particular type of system.
2. Failure and faulty component (i.e., the component responsible forthe failure) arenecessary and indissociable notions for the analysis of system behaviors.
In this work, we question these two dogmas and present a generalcomputational model,suitable for describing any type of system with benign failures, thathinges only on thenotion of transmission failure.
In this model, computations evolve in rounds, and communication missedat a roundis lost. Only information transmission is represented: for each roundr and each processp, our model provides the set of processes that p "hears of" at roundr (heard-of set)namely the processes from which p receives some message at round r.The features of aspecific system are thus captured as a whole, just by a predicate overthe collection ofheard-of sets. We show that our model handles all types of benignfailures, to be staticor dynamic, permanent or transient, in a unified framework.Using this new approach, we are able to give shorter and simplerproofs of importantresults (non-solvability, lower bounds). In particular, we prove thatConsensus cannotbe solved without an implicit consensus on heard-of sets. We alsoexamine Consensusalgorithms in our model. In light of this specific agreement problem,we show how ourapproach allows us to devise new interesting solutions.
Top

June 23, 2006, 14:00
Speaker: John Mullins
Title: Analyse de flux d'information dans les protocoles cryptographique

Abstract:
Les protocoles cryptographiques sont des règles d'échange entre les points d'un réseau qui permettent de sécuriser les communications. Il est notoire que leur conception est un exercice difficile et que la moindre faille peut avoir des répercussions économique énormes. Il n'est donc pas étonnant que ces dernières années, l'application des méthodes formelles à l'analyse des protocoles cryptographiques se soit imposée comme un champ de recherche émergent. Après un bref rappel sur les protocoles de cryptographies et des problèmes qu'ils posent au concepteur, nous présenterons plus spécifiquement les méthodes d'analyse basées sur la détection de flux d'information developpées au laboratoire CRAC de l'école Polytechnique de Montréal.
Top

Tuesday September 26, 2006, 14:00
Speaker: Tom Chothia
Title: Analysing the MUTE Anonymous File-Sharing System Using the Pi-calculus

Abstract:
This talk gives details of a formal analysis of the MUTE system for anonymous file-sharing. We build pi-calculus models of a node that is innocent of sharing files, a node that is guilty of file-sharing and of the network environment. We then test to see if an attacker can distinguish between a connection to a guilty node and a connection to an innocent node. A weak bi-simulation between every guilty network and an innocent network would be required to show possible innocence. We find that such a bi-simulation cannot exist. The point at which the bi-simulation fails leads directly to a previously undiscovered attack on MUTE. We describe a fix for the MUTE system that involves using authentication keys as the nodes' pseudo identities and give details of its addition to the MUTE system.
Top

Page maintainer: Carlos Olarte