LOGIQUE DE LA
PROGRAMMATION
Séminaires 2005-2006
|
|
|
Organisatrice : Marie-Renée Fleury-Donnadieu
(téléphone : 04 91 26 96 38).
Horaire :en règle générale le séminaire aura lieu le mardi.
Lieu : IML, Bâtiment TPR2- CNRS.
-
Amphithéatre de
l'IML : 1er étage
-
Salle de DEA et
Salle de réunion de l'équipe : 2ème étage.
-
Salle de Séminaire : 3ème étage.
* Un groupe de travail est un séminaire informel. Les exposés y sont de
durée variable et propices à des discussions.
|
Retour à la page d'accueil du Séminaire
-
Mardi 16 Mai 2006, à 14h, Amphi Herbrand
Jean KRIVINE (INRIA), page perso
Reversible Process algebra.
Résumé :
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 to derive correct
distributed systems that reduces correction to a weaker notion of
causal or forward correctness by adding implicit backtracking that is
already proved correct. We will discuss how this method could be the
basis of a PROLOG-like way of programming transactionnal systems.
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)
-
Mardi 13 Décembre 2005, à 10h, Amphi Herbrand
(Séminaire).
Marcelo FIORE (Computer Laboratory, University of Cambridge), page perso
Free groupoids: Some theory and applications (Joint work with Tom Leinster).
Résumé :
I will give an explicit description of the free monoidal groupoid on an
idempotent, showing how the subject relates to developments in geometric
group theory (R.Thompson's groups), computation (interaction nets), and
logic (geometry of interaction). Analogous constructions for symmetric
monoidal and braided monoidal categories together with applications in
type theory (type isomorphism), algorithmics (tree rotation), and category
theory (coherence) will be discussed.
-
Lundi 12 Décembre 2005, à 10h, Amphi Herbrand
(Séminaire).
Thomas STREICHER (Technische Universität Darmstadt)
page perso
Replete Topological Predomains need not be Sober. (Joint work with G. Gruenhage)
Résumé :
The notion of replete object was introduced by M. Hyland and P. Taylor
around 1990 within Synthetic Domain Theory (SDT) in analogy with the
sober spaces as known from topology. We show that for the realizability
model over Scott's graph model and Kleene's function realizability model
repletion is not given by sobrification. Thus there are replete objects
which are not sober. Moreover, we show that a certain equalizer
construction for repletion (as considered in the early days of SDT)
fails to do its job.
article
-
Lundi 28 novembre 2005, à 14h, Amphi Herbrand
(Groupe de travail).
Daniel DE CARVALHO (IML), page perso
Sémantiques non uniformes du lambda-calcul, types avec intersection et temps de calcul.
Résumé :
La sémantique relationnelle de la logique linéaire induit une sémantique du lambda-calcul pur : celle-ci est construite sur les types avec intersection
introduits par Coppo, Dezani-Ciancaglini et Venneri et on peut alors voir les termes avec ressources de Ehrhard et Régnier comme des dérivations dans ce système de typage. Par ailleurs, ce système est relié au temps d'excéution dans la machine de Krivine...
-
Lundi 19 Septembre 2005, à 14h, Amphi Herbrand
(Séminaire).
Peter HINES (Oxford University, UK)
page perso
Conditional iteration in quantum systems.
Résumé :
In this talk I describe joint work with Philip Scott, (University of Ottawa)
on conditional iteration in quantum systems. This is an investigation of
conditional iteration in purely quantum systems (rather than the familiar
"classical control - quantum data" paradigm), using tools from the theory of
reversible computation.
Although purely quantum iteration has previously been considered, and forms
an integral part of Shor's algorithm, there are several well-known problems
associated with it. We consider what these look like from a more traditional
point of view, and demonstrate a close connection with the no-deleting, or
no-contraction, theorem.
-
Mardi 20 Septembre 2005, à 14h, Amphi Herbrand
(Séminaire).
Kazushige TERUI (Keio university, Japon- Invité IML), page perso
Towards a semantic characterization of cut-elimination. (joint work with Agata Ciabattoni).
Résumé :
A huge number of logics and sequent calculi have been invented in the literature.
Among them, some enjoy cut-elimination, but the others do not.
In this talk, we consider a class of sequent calculi, each defined by a set of structural and logical inference rules, and give a necessary and sufficient condition for such a calculus to admit cut-elimination in terms of phase semantics.
Our condition is partly due to the appendix C.4 of "Meaning I" (Girard 1999). The other part is obtained by an analysis of Okada's phase-semantic proof of cut-elimination for Linear Logic.