Thesis Fellowship in Theoretical Computer Science

Thesis Fellowship in Theoretical Computer Science

[Francois Lamarche]

		THESIS FELLOWSHIP IN COMPUTER SCIENCE



A three-year fellowship is available for a thesis in Computer
Science, to be done in Nancy, in the east fo France, under the
supervision of Francois Lamarche
http://www.loria.fr/~lamarche


		SEMANTICS OF PROOFS IN CLASSICAL LOGIC


During the last 2-3 years great progress has been made in our
understanding of the semantics of proofs in classical logic [1][2][3],
but there is still a lot to be done. The general theme of this this
thesis project is the exploitation of the fruitful interaction between
denotational semantics and syntax, an direction of research which
began with the work of Dana Scott on the untyped lambda calculus, and
has seen the invention of linear logic through Girard's observation of
the category of coherence spaces and linear maps. The primary aim is
to

- first develop and write up a simple interpretation of classical
    logic in a category of posets, which is an unpublished byproduct of
    the denotational semantics given in [2],

- then apply some of the insights given by that semantics to new
    approaches to proof nets for classical logic.

Thus there is already some amount of material which simply has to be
written up as a springboard, and should help the student pick up
momentum before doing truly original research (we hasten to mention
that a full mastery of the rather formidable [2] is not necessary at
first for doing so). But the real interest of a thesis is to give
students the occasion to prove their mettle, and we foresee plenty of
openings here for doing that, with several open questions on
correctness criteria, complexity, proof search, etc. In particular
there is the tantalizing possibility of using non-commutative logics
(that use braidings) to give a practical solution to the difficult
problem of counting the number of axiom links that are used in a
classical proof, which has connections to deep problems in complexity
theory.


     Work and study environment

The student would be registered at the Computer Science department one
of the universities (or engineering school) which belong to the joint
graduate studies program of the IAEM doctoral school.  A sizeable
proportion of the students registered in that school come from outside
of France and Europe. Students are required to follow a moderate
number of graduate courses, which are usually given in French.  There
are special programs aimed specifically atforeign graduate students,
to help them learn French.

Work will be done at the Loria laboratory of computer science
http://www.loria.fr in Nancy, on the science campus. The student will
be part of the Calligramme research project at INRIA-Lorraine.  The
student will be able to interact with everal research projects dealing
with theoretical issues in computer science.

The fellowship guarantees financing for three years; the student who
does not complete the thesis work in that time span will be able to
extend his/her stay through teaching contracts; but theses that last
more than four years are exceptional and not encouraged by the
authorities.

    Profile sought

The candidate is required to have a Master's degree in Mathematics or
Computer Science, with an orientation towards theoretical computer
science. More precisely we expect experience in one or several of the
the following topics: linear logic, the theory of {interaction, proof}
nets, category theory, denotational semantics. An acquaintance with
basics of deep inference is also a big plus.

    Procedure

Putative candidates are requested to send an email to
François Lamarche for further enquiry

(look at http://www.loria.fr/~lamarche  for exact email address
and http://www.loria.fr/~lamarche/TheseEnglish.html
for the html version of this announcement.)

[1] C. Fuhrmann and D. Pym: Order-enriched categorical models of the
     classical sequent calculus. *J. Pure and App. Algebra 204(1)*.

[2] F. Lamarche: Exploring the gap between linear and classical
logic. *Accepted for publication in Theory and Applications of
Categories*.

[3] F. Lamarche and L. Strassburger: Naming proofs in classical  
logic, *TLCA 2005,
in SLNCS 3461*