
Calendar2012 2011 2010 2009 2008 2007 2006 2005 2004AbstractsHR> Nov 20 2007, 14:00Speaker: Simon Kramer Title: Towards Interactive Belief, Knowledge, and Provability: Possible Application to ZeroKnowledge Proofs Abstract: We argue that modal operators of interactive belief, knowledge, and provability are definable as natural generalisations of their noninteractive counterparts, and that zeroknowledge proofs (from cryptography) have a natural (modal) formulation in terms of interactive individual knowledge, noninteractive propositional knowledge and interactive provability. Our work is motivated by van Benthem's investigation
into rational agency and dialogue and our attempt to
redefine modern cryptography in terms of modal logic.
Nov 15 2007, 14:00 Speaker: Antonino Salibra Title: Algebra and topology in lambda calculus Abstract: In this seminar we show how algebra and topology can be fruitfully applied to the operational semantics and to the model theory of the untyped lambda calculus. It will be also analyzed one of the longstanding open problem of lambda calculus, regarding the existence of a topological model of the betaeta lambda theory, where all Scottcontinuous functions are representable. Oct 29 2007, 14:00 Speaker: Michael Mislove Title: Probabilistic Input/Output Automata From a Domaintheoretic Perspective Abstract: Probabilistic Input/Output Automata (PIOAs) are probabilistic systems that were initially devised by Roberto Segala and have been used as model in a variety of computational settings. Most recently, a variant called Task PIOAs have been used to model cryptoprotocols in a way that allows for a finer analysis of lower level mechanisms that underlie modern cryptography. In particular, the approach supports allows the power of the adversary to be restricted while also supporting reasoning about probabilistic polynomial time computations and simulations that are negligible with respect to a meaningful metric. In this talk, I'll describe a domaintheoretic approach to PIOAs that allows a simple derivation of some of the key mathematical results about their structure.
This is joint work with Aaron Jaggard (DIMACS) and Catherine Meadows (NRL).
Oct 16 2007, 14:00 Speaker: Andrea Turrini Title: Security Protocol Verification with Probabilistic Automata Abstract: We study simulation relations for Probabilistic Automata that require transitions to be matched up to negligible sets provided that computation lengths are polynomially bounded. These relations are meant to provide rigorous grounds to parts of correctness proofs for cryptographic protocols that are usually carried out by semiformal arguments. We illustrate our ideas by recasting a correctness proof of Bellare and Rogaway based on the notion of matching conversation.
Paper available here
Oct 11 2007, 14:00 Speaker: Nicolas Guenot Title: MultiFocusing in Deep Inference Abstract: The calculus of structures has interesting properties of symmetry, due to its deep inference feature, which allows to work inside a formula without destroying the toplevel connectives. In this talk, we will discuss the problem of defining formally what "focusing" could be, and how this generic idea can be translated into the calculus of structures. We will then describe a focused system for MALL in CoS which naturally comes with the multifocusing extension, where several formulas could live under a focusing arrow at the same time (under the same arrow in the sequent calculus, under several arrows in CoS). This system is quite simple, has two symmetric reaction rules unlike Andreoli's system and doesn't need a decision rule. We will finally present the open topics related to this system, such as the search for a completeness proof inside the calculus of structures, which would be more elegant than the translation from the sequent calculus used so far. Oct 05 2007, 14:00 Speaker: Simon Kramer Title: Animation and Knowledge Programming for the Timed Calculus of Cryptographic Communication Abstract: We give an overview of the Timed Calculus of Cryptographic Communication, one of the very few process calculi for security with realtime capabilities, and argue that the addition of knowledge programming capabilities to our calculus is easy. We intend to animate the calculus via logic programming. URLs: (Thesis, Chapter 4.1 and 4.2) Oct 02 2007, 14:00 Speaker: Simon Kramer Title: The Intended and Actual Meaning of a Cryptographic Message and Protocol Abstract: We propose a denotational definition for the (actual) meaning of a cryptographic message and, based on it, an equational definition for the contextsensitivity of that meaning, both via hypothetical knowledge and provability. As a result, we obtain a formalisation of the first of Abadi and Needham's principles for prudent engineering practice for  and a tentative denotational semantics of  cryptographic protocols. Building on this (published) work, we present ongoing work on the distinction between the intended and the actual meaning of a cryptographic message and protocol." URLs: (Thesis, Chapter 4.3) (FCSARSPA'07 respectively LORI'07)
Jun 19 2007, 14:00 Speaker: Cosimo Laneve Title: The must preorder revisited  an algebraic theory for web services contracts. Abstract: We define a language for Web services contracts as a parallelfree fragment of CCS and we study a natural notion of compliance between clients and services in terms of their corresponding contracts. The induced contract preorder turns out to be valuable in searching and querying registries of Web services, it shows interesting connections with the must preorder, and it exhibits good precongruence properties when choreographies of Web services are considered. Our contract language may be used as a foundation of Web services technologies, such as WSDL and WSCL.
HTTP: cs.unibo.it/PiDuce
Jun 12 2007, 14:00 Speaker: Josef Widder Title: Consensus in the Presence of Value Faults. Abstract: The problem of agreeing on a common value (consensus) encapsulates the inherent problem of building reliable, i.e., fault tolerant systems. The faults considered in this talk can be subsumed under value faults; informally, from the viewpoint of the receiver of some message, the content of the message may be different from what would have been received in the absence of faults (i.e., if every component on the path of the message has worked according to its specification).
The first part of the talk will consider a novel failure model (called
mortal Byzantine) which captures all process failures which eventually
lead to the crash of the faulty process. By considering an optimal
consensus algorithm which tolerates this failure model, we motivate a
more general formalism which should allow to investigate the
requirements of consensus regarding the communication structure in a
distributed computation. In the second part of the talk we will
introduce such a formalism (the heardof model incorporating value
faults) which allows to separate the requirements on the communication
regarding safety and liveness of consensus while capturing dynamic and
transient link and process failures.
Jun 07 2007, 15:00 Speaker: Daniele Varacca Title: Event structure semantics of the picalculus. Abstract: We propose the first compositional event structure semantics for a fully expressive picalculus, generalising Winskel's event structures for CCS. The picalculus we model is the picalculus with recursive definitions and summations. First we model the synchronous calculus, introducing a notion of dynamic renaming to the standard operators on event structures. Then we model the asynchronous calculus, for which a new additional operator, called rooting, is necessary for representing causality due to new name binding. The semantics are shown to be operationally adequate and sound with respect to bisimulation. Jun 04 2007, 15:00 Speaker: Vladimiro Sassone Title: A Bayesian model for eventbased trust. Abstract: We focus on systems where trust in a computational entity is interpreted as the expectation of certain future behaviour based on behavioural patterns of the past, and concern ourselves with the foundations of such probabilistic systems. In particular, we aim at establishing formal probabilistic models for computational trust and their fundamental properties. In the paper we define a mathematical measure for quantitatively comparing the effectiveness of probabilistic computational trust systems in various environments. With this foundation in place, we formalise a general notion of information about past behaviour, based on event structures. This yields a flexible trust model where the probability of complex protocol outcomes can be assessed. May 31 2007, 14:00 Speakers: Kaustuv Chaudhuri and Joelle Despeyroux Title: A Hybrid Temporal Logical Framework for Systems Biology. Abstract: We propose a logical framework for reasoning in and about systems biology. Our framework is based on Girard's linear logic, extended with modal situated truth and a temporal interpretation of the modal worlds. The ``current world'' (or instant of time) can be referred to in the logic using the localisation operator from hybrid logic, which allows us to describe the delays in a process and hence the rates of reactions. The resulting logic gives a uniform language for both stochastic descriptions, such as those based on the Picalculus, and continuous ODE descriptions. May 29 2007, 14:00 Speaker: Alexandre Miquel Title: The experimental effectiveness of mathematical proofs. Abstract: The CurryHoward correspondence interprets each mathematical proof as a program realizing some specification (deduced from the proved formula). But what happens when the proof relies on experimental assumptions  for instance laws of physics? In this talk, I propose to study the frontier between mathematical reasoning and the empirical hypotheses underlying natural sciences. For that, I will start from a problem posed by the philosopher Karl R. Popper on the use of abstract mathematical tools in an empirical framework. I will then show how modern realizability techniques can be used to solve this problem, suggesting new ways of combining mathematical reasoning with experimental protocols effectively. May 03 2007, 14:30 Speaker: Robin Milner Title: An Introduction to Bigraphs. Abstract: Bigraphs are a generic model for mobile interactive systems. They have three aims: (1) To give a uniform treatment of behavioural equivalences and preorders in process calculi; (2) To provide a way to models realworld mobile systems, whether natural or constructed; (3) To provide a programming or descriptive tool that will allow real systems or specifications to be executed, or simulated. This is the first of three talks on bigraphs in May, and I shall describe bigraph structure and dynamics slowly, with as much intuition as possible. I hope I'll get far enough to explain how to exactly recover bisimilarity for finite CCS in this general framework. This serves (1) above. The second talk, by Arne Glenstrup on May 10, will serve (2) by explaining how bigraphs are implemented at ITU Copenhagen.
The third talk, by Jean Krivine on May 22, will serve (3) by modelling
some biology.
May 10 2007, 14:30 Speaker: Arne Glenstrup Title: Implementing Matching of Binding Bigraphs. Abstract: The Bigraphical Programming Languages (BPL) Project at the IT University of Copenhagen aims to do research into how programming languages for mobile and contextaware applications can be based on the theory of bigraphs. As a first attempt to operationalise bigraphs, we have implemented a tool for representing and manipulating binding bigraphs. The implementation stands out as being closely based on bigraph theory formally proven correct. It includes representations of normal and regular forms, as well as algorithms for normalisation and regularisation. The keystone that enables simulation of bigraphical reactive systems is a matching algorithm which is based on an inference system that has been formally proven sound and complete [1]. This talk will report on major aspects of the ongoing implementation work. This is joint work with Lars Birkedal, Troels Christoffer Damgaard and Espen Hojsgaard.  [1] Birkedal, L., Damgaard, T. C., Glenstrup, A. J., and Milner, R. (2006b). Matching of bigraphs. In Proceedings of Graph Transformation for Verification and Concurrency Workshop 2006, Electronic Notes in Theoretical Computer Science. Elsevier. May 22 2007, 14:30 Speaker: Jean Krivine Title: A platform for the Simulation and analysis of bio molecular systems in the kappacalculus. Abstract: Joint work with Vincent Danos (Laboratoire Preuves Programmes et Systemes,CNRS, France), Jerome Feret (Ecole Normale Superieure, Paris), Walter Fontana (Systems Biology Department, Harvard Medical School, US). In this talk we present a tool currently in development at Plectix Biosystems (Boston, US) allowing to analyse and simulate large bio molecular systems. The tool relies on an agent based formalism called kappa [1]. We first present the language in which states, called solutions or systems, are graphs where connections are made on sites and transitions are generated by a restricted class of graphrewriting rules. We will see that this language can be neatly represented and extended using bigraph formalism. We will then proceed with the description of the stochastic simulation algorithm. [1] Formal Molecular Biology (TCS 325, 2004) Vincent Danos, Cosimo Laneve Mar 13 2007, 14:00 Speaker: Ichiro Hasuo (Jointwork with Yoshinobu Kawabe at NTT Corporation, Japan) Title: Probabilistic Anonymity via Coalgebraic Simulations. Abstract: There is a growing concern on anonymity and privacy on the Internet, resulting in lots of work on formalization and verification of anonymity. Especially, importance of probabilistic aspect of anonymity is claimed recently by many authors. Among them are Bhargava and Palamidessi who present the definition of probabilistic anonymity for which, however, proof methods are not yet elaborated. In this paper we introduce a simulationbased proof method for probabilistic anonymity. It is a probabilistic adaptation of the method by Kawabe et al. for nondeterministic anonymity: anonymity of a protocol is proved by finding out a forward/backward simulation between certain automata. For the jump from nondeterminism to probability we fully exploit a generic, coalgebraic theory of traces and simulations developed by Hasuo, Jacobs and Sokolova. In particular, an appropriate notion of probabilistic simulations is obtained by instantiating a generic definition with suitable parameters.
REFERENCE:
Ichiro Hasuo and Yoshinobu Kawabe.
Probabilistic Anonymity via Coalgebraic Simulations.
To appear in Proc. ESOP 2007.
Feb 14 2007, 15:00 Speaker: Daniele Gorla Title: On the Relative Expressive Power of Calculi for Mobility. Abstract: In this talk, we shall comparatively analyse some mainstream calculi for mobility: the picalculus, the distributed picalculus, a distributed version of Linda and Mobile/Boxed/Safe ambients. In particular, we shall focus on their relative expressive power, i.e. we shall try to encode one in the other while respecting some reasonable properties. By means of 'good' encodings, or impossibility of such results, we set up a hierarchy of these languages. Finally, we discuss and compare several variants of ambientlike languages, including objective moves, passwords and different semantics for the mobility primitives and for parentchild communications. Page maintainer: Carlos Olarte 