|
|
|
| DIPARTIMENTO DI INFORMATICA Università di Torino |
|
|
|
|
 Research on "Semantics and Logics of Computation" Next Seminars Friday May the 22nd, 2009. 11:00am - Sala Seminari Full resource calculus by Paolo Tranquilli - PPS - Paris VII University Abstract: In 1993 Gerard Boudol introduced a variant of the lazy lambda calculus called lambda calculus with resources. In this calculus arguments can be mixed together and have a limited availability (whence nondeterminism). Recently differential lambda calculus by Ehrhard and Regnier has been found to be strikingly linked to Boudol's calculus, leading to a reformulation of both. We thus present here an overview of the full, non lazy resource calculus: syntax, reduction, typing, a sketch of its link with differential nets and its confluence and termination properties. Link: home page Monday May the 25th, 2009. 11:00am - Sala Seminari Membrane computing by Caludio Zandron - Milano-Bicocca University Abstract: Computing with membranes is a recent branch of Molecular Computing, proposed at the end of 1998 by Gh. Paun, and inspired from the structure and the functioning of the cell. In the compartments defined by a membrane structure one has multisets of symbol-objects which evolve according to given rules also associated with each compartment, and then are communicated through membranes. The membrane structure can be modified by dissolving or dividing membranes. The evolution rules are applied in a nondeterministic, maximally parallel manner: in each time unit, all objects which can evolve should do it. In this way, transitions from a configuration of the system to another configuration are defined; a sequence of transitions defines a computation. A result is associated with a halting computation in the form of the vector of natural numbers describing the multiplicity of certain objects in a certain membrane. Main results concerning the obtained computational model will be given, as well as its application to systems biology. Past SeminarsPrimitive recursion in finiteness spacesThe category FIN of finiteness spaces and finitary relations introduced by Ehrhard provides a model of linear logic, which refines the purely relational one. By the usual co-Kleisli construction, it also provides a model FIN! of the simply typed lambda-calculus. Although it is known that the standard fix-point operators are not finitary, Ehrhard proved that a limited form of recursion was available, by defining a finitary tail-recursive iteration operator. We prove that finiteness spaces can actually accomodate the standard notion of primitive recursion: the cartesian closed category FIN! admits a weak natural number object, in the sense of Thibault (82) and Lambek-Scott (88), which allows to model the iterator version of Gödel's system T. We also exhibit a recursor operator using the same object. This work is carried out in the qualitative version of finiteness spaces, but it should be understood as a first step towards a quantitative semantics of primitive recursion in the algebraic version. With this goal in mind, we will discuss the relevance of our approach. Speaker: Lionel Vaux, Université de Savoie Date and time: Apr. the 21st, 2009. 10:30am Where: Sala Seminari Links: home page The duality of computation under focus We use the infrastructure of Curien-Herbelin's $\lbdmmtld$-calculus to provide a syntax for a (weakly) focalised version of LK, which we call LKQ given its close relation with Danos-Joinet-Schellinx's LKQ. We then move on to a fully focalised syntax close to Girard's ludics and Zeilberger's CU. We also provide a version of our syntax closer to Girard's original LC (the first constructivisation of classical logic) and show its usefulness as the target of a translation of a mixed call-by-name/call-by-value language. Speaker: Pierre-Louis Curien, PPS, Paris VII University Date and time: Feb. the 9th, 2009. 15:30pm Where: Sala Riunioni Use of process algebra in security problems (information flow / privacy) Speaker: Catuscia Palamidessi, INRIA-Futurs e LIX Date and time: Feb. the 9th, 2009. 14:30pm Where: Sala Riunioni Modeling the Handshake Protocol for Asynchrony - Phd dissertation Abstract: This thesis deals with communication protocols in an asynchronous environment. Within asynchrony it is particularly important to ensure the absence of computation and transmission interference. Computation interference occurs when a message is sent to an unready receiver, while transmission interference occurs when a channel carries more than one message. Asynchronous communication protocols should ensure that neither of the above situations takes place. A protocol is said to be speed-independent if it ensures correctness independently of the computational speeds of single modules. A speed-independent protocol ensures the absence of computation interference. A protocol is said to be delay-insensitive if it is speed-independent and, moreover, it ensures correctness independently of propagation delays in the communications. A delay-insensitive protocol ensures the absence of both computation and transmission interference. The thesis is composed of two parts. In the first part we briefly survey some existing formalisms and tools which underlie many models of asynchronous communication and we formally introduce the notions of speed-independence and delay-insensitivity. Then in the second part we focus on the handshake protocol, a particular kind of delay-insensitive protocol which requires that the two partners involved in each communication alternate. Applications of this simple paradigm have been central in the development of asynchronous VLSI chips. The aim of the thesis is to provide solid theoretical foundations to a communication discipline which was exported so quickly to applications that its formal analysis has been left behind. In this perspective we introduce three different representations of handshake protocols: a game-semantics, a Petri nets model and a process calculus (the last two in collaboration with Daniele Varacca). The game semantics fixes a bug in the definition of composition which was present in a previous trace model of the handshake protocol. However, it fails to represent some handshake behaviors. The Petri nets model instead, is correct and complete with respect to all handshake behaviors. We also propose a process calculus in CCS style and we show its correctness as a syntax for the handshake protocol. We provide an interpretation from the calculus to the Petri nets model, which is fully abstract and such that any finite net is the interpretation of some ?configuration? in the calculus. Speaker: Luca Fossati, Torino University and Paris VII University Date and time: Feb. the 9th, 2009. 10:30pm Where: Sala Riunioni A realizability intepretation for Heyting Arithmetic with excluded middle over Sigma-0-1 formulas Abstract: We introduce a new notion of realizability for Heyting Arithmetic plus Excluded middle axiom restricted to Sigma-0-1 formulas (HA + EM1). Our work is based on the notion of atomic realizability introduced in “A calculus of realizers for EM1-Arithmetic” (CSL 2008) by Berardi and de'Liguoro for quantifier free primitive recursive Arithmetic plus EM1, and extends and adapts it in a non trivial way to full predicate logic. Our notion extends Kleene's realizability and differs from it only in the atomic case: we interpret atomic realizers as learning agents. We show how to extract realizers from classical proofs and how they intuitionistically realize Pi-0-2 formulas. Links: slides - article Speaker: Federico Aschieri, Torino University (Joint work with Stefano Berardi) Date and time: Feb. the 6th, 2009. 11:30pm Where: Sala Seminari A Multimodal
Stratified framework for
polynomial time sound computations
|
[Research on "Semantics and Logics of Computation"] [Department's HOME]
|
|
|
| Last update: May 8, 2009 | |
|
|
|