Colloquium Pierre Lescanne (2008) Nancy
|
This page comes from : |
Contents
A journey through term rewriting and lambda-calculi
Colloquium in Honor of Pierre Lescanne
May 29, 2008 - LORIA, Nancy
This one-day Workshop will feature a series of state-of-the-art invited talks on current research trends in automated deduction, term rewriting and lambda-calculi. The Workshop will celebrate the contribution of Pierre Lescanne to different subjects of automated deduction, as well as his past and ongoing contributions to running scientific groups, managing scientific projects on national and international levels, supervising PhD students, and promoting science.
Invited speakers
- Claude Pair Nancy
- Paliath Narendran SUNY Albany
- Nachum Dershowitz Tel-Aviv University
- Mariangiola Dezani Torino University
- Jean-Pierre Jouannaud Ecole Polytechnique
- Hélene Kirchner CNRS/INRIA
- Dan Dougherty Worcester Polytechnic Institute
- Simona Ronchi Della Rocca Torino University
Workshop program
9:00 -- 9:10 Welcome: Karl Tombre & Organizers
9:10 -- 10:30 Session 1
Claude Pair. Que faisions-nous et qu'était le CRIN a l'arrivée de Pierre ?
Nachum Dershowitz. Church's Lambda Calculus and Church's Thesis. We discuss the pros and cons of the lambda calculus as a model of computation. We propose a generic axiomatization ofeffective computation, adding a condition on initial states to Gurevich's "Abstract State Machine" postulates. Axiomatization in hand, we prove the Church-Turing Thesis. (Joint work with Yuri Gurevich and with Udi Boker)
10:30 -- 11:00 Break
11:00 -- 13:00 Session 2
Mariangiola Dezani. Global Progress in Dynamically Merged Multiparty Sessions. This work develops, besides a more traditional communication type system, a novel static interaction type system for global progress in dynamically merged and interfered multiparty sessions. High-level session processes equipped with global signatures are translated into low-level processes, in which type-soundness is guaranteed against the local, compositional type system. This avoids a global linearity-check without scarifying the original expressivity. The interaction type system automatically infers causalities of channels for the low level processes, ensuring the entire protocol, starting from the high-level processes which consist of multiple sessions, does not get stuck at intermediate sessions also in presence of delegation.
Dan Dougherty. We present some preliminary ideas relating the notion of strategy in rule-based languages and the classical notion of strategy in games such as those arising in descriptive set theory, planning, and verification.
Paliath Narendran. Intruders with Caps. In the analysis of cryptographic protocols, a treacherous set of terms is one from which an intruder can get access to what was intended to be secret, by adding on to the top of a sequence of elements of this set, a cap formed of symbols legally part of his/her knowledge We discuss conditions on the rewrite system modeling the intruder's abilities to ensure that it is decidable if such caps exist.
14:10 -- 15:30 Session 3
Simona Ronchi Della Rocca. Soft Linear Logic and Polynomial Complexity classes. We will describe some results inspired from Lafont's Soft Linear Logic which is a subsystem of second-order linear logic with restricted rules for exponentials, correct and complete for polynomial time computations.
Jean-Pierre Jouannaud. From finite to transfinite to finite semantic trees.
16:00 -- 17:20 Session 4
Hélene Kirchner. Strategic rewriting and narrowing. The talk will propose definitions of these concepts, will illustrate their interest in several contexts and will raise some open questions.
Jacques Jaray. Mon ami Pierre
18:00 Reception
Organizing committee
- Anne-Lise Charbonnier, (LORIA),
- Guillaume Bonfante, (LORIA),
- Philippe Degroote, (LORIA),
- Francis Klay, (France Telecom),
- Gregory Kucherov, (LIFL/CNRS),
- Luigi Liquori, (INRIA Sophia Antipolis - Méditerrannée),
- Jean-Yves Marion, (LORIA),
- M. Rusinowitch, (LORIA),
- Laurent Vigneron, (LORIA)
