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*