
Calendar2012 2011 2010 2009 2008 2007 2006 2005 2004AbstractsDec 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 sublanguages of the Ambient Calculus, and a study of the expressive power of polyadic synchronization in picalculus 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 picalculus, 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. 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. 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 faulttolerant 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.
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 tableaubased 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. 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. Thursday Nov 23 2006, 14:00 Speaker: Pierre Sutra Title: Eventual consistency and commitment in semanticallyrich 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. 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. 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 modelchecking techniques, and how to compute the capacity in some particular cases. We will illustrate this methodology on the wellknown 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 wellknown 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. 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 nondeterministic dataflow; the unfolding of Petri nets; the semantics of higherorder processes; equivalences. Tuesday Oct 17, 2006, 14:00 Speaker: Chuck Liang Title: AspectOriented Programming in HigherOrder and Linear Logic Abstract: "Aspectoriented 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 higherorder 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. Wednesday Oct 25 2006, 15:00 Speaker: Frank Valencia Title: On Linearity vs Persistence and a FOL Interpretation of the picalculus Abstract: We shall present an expressiveness study of linearity and persistence of processes. We choose the picalculus, one of the main representatives of process calculi, as a framework to conduct our study. We consider four fragments of the picalculus. 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 nonexistence of) encodings among the fragments, a processesasformulae interpretation and a reduction from Minsky machines. The fragments are: (1) The (polyadic) asynchronous picalculus Api, (2) persistentinput Api defined as Api with all inputs replicated, (3) persistentoutput Api defined as Api with all outputs replicated, and (4) persistent Api defined as Api with all inputs and outputs replicated. We provide compositional fullyabstract 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 Turingpowerful. We further show that barbed congruence is undecidable for the zeroadic version of (2), the monadic version of (3) and the biadic version of (4). In contrast, we also show that it is decidable for the zeroadic versions of (3) and (4). Furthermore, we provide a compositional interpretation of the pi processes in (4) as FirstOrder 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 picalculus 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 infinitestate processes exhibiting meaningful mobile behaviour. Jan 10, 2006 Speaker: Gopalan Nadathur Title: Practical HigherOrder Pattern Unification with OntheFly Raising Abstract: Higherorder 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 "forallsomeforall" 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 lowlevel 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 onthefly 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 higherorder 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] 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 patternmatching. 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 picalculus. 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 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 ) 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. 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. May 9, 2006, 14:00 Speaker: Steve Kremer Title: CoercionResistance and ReceiptFreeness in Electronic Voting Abstract: We formally study important properties of electronic voting protocols. In particular we are interested in coercionresistance and receiptfreeness. Intuitively, an election protocol is coercionresistant 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. Receiptfreeness is a weaker property, for which we assume that A and C cannot interact during the protocol: to break receiptfreeness, A later provides evidence (the receipt) of how she voted. While receiptfreeness can be expressed using observational equivalence from the applied pi calculus, we need to introduce a new relation to capture coercionresistance. Our formalization of coercionresistance and receiptfreeness are quite different. Nevertheless, we show in accordance with intuition that coercionresistance implies receiptfreeness, 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. May 11, 2006, 11:00 Speaker: Sebastien Briais Title: Open Bisimulation, Revisited Abstract: In the context of the picalculus, open bisimulation is prominent and popular due to its congruence properties and its easy implementability. Motivated by the attempt to generalise it to the spicalculus, 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 spicalculus. 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 TuringPowerful formalism into a one which sits below CFL in the Chomsky Hierarchy. 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. June 15, 2006, 14:00 Speaker: Bernadette CharronBost Title: The Iconoclast HearOf Model: Unifying all Benign Failures Abstract: Problems in faulttolerant 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 (heardof 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 ofheardof 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 (nonsolvability, lower bounds). In particular, we prove thatConsensus cannotbe solved without an implicit consensus on heardof 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. 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. Tuesday September 26, 2006, 14:00 Speaker: Tom Chothia Title: Analysing the MUTE Anonymous FileSharing System Using the Picalculus Abstract: This talk gives details of a formal analysis of the MUTE system for anonymous filesharing. We build picalculus models of a node that is innocent of sharing files, a node that is guilty of filesharing 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 bisimulation between every guilty network and an innocent network would be required to show possible innocence. We find that such a bisimulation cannot exist. The point at which the bisimulation 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. Page maintainer: Carlos Olarte 