[Prev][Next][Index][Thread]
POSTDOC still available...until Friday the 1st ...

To: types@cis.upenn.edu, lprologlist@cis.upenn.edu, theoremprovers@ai.mit.edu, compunode@compulog.org, bratypes@cs.chalmers.se, elflist@cs.cmu.edu, coqclub@pauillac.inria.fr, pvs@csl.sri.com, logic@cs.stanford.edu, qed@mcs.anl.gov, THEORYA@LISTSERV.NODAK.EDU, david@univsavoie.fr, Christophe Raffalli <Christophe.Raffalli@univsavoie.fr>

Subject: POSTDOC still available...until Friday the 1st ...

From: Christophe Raffalli <Christophe.Raffalli@univsavoie.fr>

Date: Wed, 30 Aug 2000 16:13:22 +0200

Organization: Laboratoire de =?iso88591?Q?Math=E9matiques?=, =?iso88591?Q?Universit=E9?= de Savoie

Sender: raffalli@central.cis.upenn.edu
[Note that this is an extension of the original deadline. BCP]
=====================================================================
== Postdoc Position ==
== available at ==
== the University of Chambery (France) ==
=====================================================================
A One Year postdoctoral scholarship is available at the Logic/Computer
Science Group of the Math Laboratory in Chambery
(http://www.lama.univsavoie.fr).
Job description

Our group works on LambdaCalculus, Proof theory and their
applications to the design of a proof assistant. We are about to
release a new version of a proof assistant of the next generation:
http://www.lama.univsavoie.fr/~RAFFALLI/af2.html.
In our mind, the intended applications of a proof assistant are:
 Education: Teach students what is a correct reasoning.
 Computer Science: Specifications and proof of programs or protocols.
The candidate should work on one of the following aspect of this
project (we would also consider candidates willing to work on other
related subject) :
 Improvement of the interface designed for first year math
student: this system has been successfully experimented with third
year students but a more intuitive interface is necessary for younger
students.
 Theoretical work and implementation of a better module
system and a better equationnal reasoning. In order to make proof
development easier, these aspects are crucial and really need
theoretical research.
 Development of a library of basic mathematical results.
 Theoretical work related to proving or extracting programs.
We wish the candidate to work on both aspects (theoretical and
implementation) but applications of candidates skilled in only one of
these aspects are also welcome.
The background and experience of the ideal candidate should include
 lambdacalculus.
 logic: predicate and propositional calculus, proof theory, ...
 programming in a language of the ML family.
Administrative data

 Approximative net income: 12,000 FF (1,800 Euros) per month.
 Deadline for application: Friday September the first 14PM (french
time).
 Beginning of the position: before December 1st, 2000.
 No teaching required
Location

Chambery is a multidisciplinary university of 12,000 students in the
French Alps. The scientific campus is located close to the Lake of Le
Bourget in the Parc Scientifique Savoie Technolac. The web site of
the laboratory is: http://www.lama.univsavoie.fr
Contact

If you are interested, please contact:
 C Raffalli :
tél: (33) 4 79 75 81 03,
fax: (33) 4 79 75 87 42,
mail: Christophe.Raffalli@univsavoie.fr
 R David :
tél: (33) 4 79 75 87 17,
fax: (33) 4 79 75 87 42,
mail: Rene.David@univsavoie.fr