POSTDOCTORAL FELLOWSHIP We would like to announce an offer for a one-year postdoctoral fellowship, extensible potentially to two years. The candidate will work in Nancy, in the east of France, under the supervision of François Lamarche in the INRIA project Calligramme. Deadline for submission is MARCH 31 1007. Applications should be done through the web, via http://www.inria.fr/travailler/opportunites/postdoc/postdoc.en.html under the category "symbolic systems". There more instructions are given about the requirements. The principal constraint is that the candidate's doctoral thesis should have been defended after May 2006, and if it is still pending, that there should an official guarantee that it will be defended before September 2007. François Lamarche Francois.Lamarche@loria.fr http://www.loria.fr/~lamarche ******************************************************************* PROOF NETS FOR CLASSICAL LOGIC AND DIFFERENTIAL INTERACTION NETS. This project aims at obtaining a better understanding of the computational character of the proof nets for classical propositional logic that were introduced in [1,2]. Their current execution semantics is based on the "interaction formula" of the Geometry of Interaction, but we are still missing reduction techniques on these nets based on graph rewriting. Differential interaction nets [4], obtained from a denotational semantics based on topological vector spaces [5] share several properties with "classical" nets: both involve bialgebras in their semantics, and thus both are equiped with with a "superposition" (or convolution) operation on proofs. The aim of this project is to leverage the experience and results already obtained about the computational meaning of differential nets in the field of "classical" proof nets. Several questions are considered, but in particular -- Is it possible to apply the non-deterministic character of differential nets (visible in the interpretations of the pi-calculus that they give rise to) to "classical" nets? In other words, can the convolution operation of classical nets be given an interpretation in terms of superposition of possibilities? How far can we (or must we) push non-determinism, only in the execution process itself, or as far as the possibility of having variation in the final result of the execution? Several technical difficulties have to be overcome. We see in particular the fact that the superposition operation in "classical" nets does not have a zero. We must see how far the simile can be pushed. This is a theoretical research project, and it is impossible to give a detailed work plan. The candidate will be working in project-team Calligramme, where researchers have competence in category theory, proof nets and lambda-mu calculus and other computational models of classical logic. The candidate will also be able to interact with members of project-teams Cartes (complexity, light linear logic) and Protheo (rewriting, rho calculus). - Profile sought: We are expecting from the candidate experience in denotational semantics AND (proof, interaction) nets. Skills in category theory are also a big plus. [1] F. Lamarche and L. Strassburger: Naming proofs in classical logic. TLCA 2005 [2] F. Lamarche and L. Strassburger: Constructing free Boolean categories. LICS 2005 [3] Girard, J.-Y.: Geometry of Interaction I: Interpretation of System F. Logic Colloquium 88, North-Holland. [4] Th. Ehrhard and Laurent Regnier: Differential Interaction Nets. Theor. Comp. Sci., to appear, available on the authors' home page. [5] Th. Ehrhard: On Köthe sequence spaces and linear logic: Math. Struct. in Comp. Sci, 12, 2002. - contact (tél et e-mail) : lamarche@loria.fr, +33 (0)3 54 95 84 10 - http:www.loria.fr/~lamarche *************