Postdoctoral Fellowship in France

Postdoctoral Fellowship in France

[Francois Lamarche]

		       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

*************