[Prev][Next][Index][Thread]
Post-Doc in France available.
-
To: types@cis.upenn.edu, lprolog-list@cis.upenn.edu, theorem-provers@ai.mit.edu, compunode@compulog.org, bra-types@cs.chalmers.se, elf-list@cs.cmu.edu, coq-club@pauillac.inria.fr, pvs@csl.sri.com, logic@cs.stanford.edu, qed@mcs.anl.gov, THEORY-A@LISTSERV.NODAK.EDU, david@univ-savoie.fr, Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>
-
Subject: Post-Doc in France available.
-
From: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>
-
Date: Mon, 22 May 2000 17:43:21 +0200
-
Organization: Laboratoire de =?iso-8859-1?Q?Math=E9matiques?=, =?iso-8859-1?Q?Universit=E9?= de Savoie
-
Sender: raffalli@univ-savoie.fr
=====================================================================
== Post-doc Position ==
== available at ==
== the University of Chambery (France) ==
=====================================================================
A One Year post-doctoral scholarship is available at the Logic/Computer
Science Group of the Math Laboratory in Chambery.
Job description
---------------
Our group works on Lambda-Calculus, 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.univ-savoie.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:
- 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
- lambda-calculus.
- 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: July 15th.
- Beginning of the position: before December 1st, 2000.
- No teaching required
Location
--------
Chambery is a multi-disciplinary 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.univ-savoie.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@univ-savoie.fr
- R David :
tél: (33) 4 79 75 87 17,
fax: (33) 4 79 75 87 42,
mail: Rene.David@univ-savoie.fr