[TYPES/announce] Postdoc Position

[Ugo Dal Lago]

------------------------------------------------------------
    NEW POSTDOC POSITION IN THE "ETERNAL" INRIA ARC Project
                http://eternal.cs.unibo.it/
------------------------------------------------------------

--> Approximate period: 01/10/2011-01/10/2012 (one year) <--
-->  Deadline for submission of candidatures: 31/05/2011 <--

We are currently looking for candidates for a postdoc position,
to work on the "ETERNAL" INRIA ARC Project. The postdoc will join
the FOCUS team at the University of Bologna (http://focus.cs.unibo.it),
but short visits are possible to the other two teams participating
to "ETERNAL" (PARSIFAL and PI.R2). The postdoc will not have any
teaching duty. The gross salary will be approximately 2600 euros per
month, like any other INRIA postdoc.

REQUIREMENTS:
We are looking for candidates with a Ph.D. in Computer Science and
previous experience in either Implicit Computational Complexity
or Interactive Theorem Proving. Candidates that will defend their
Ph.D. thesis before October 2011 will also be considered.

STARTING DATE:
The proposed starting date is October 1st, 2011, but can be postponed
until the end of the year.

PROJECT DESCRIPTION:
This project aims at putting together ideas from Implicit Computational
Complexity and Interactive Theorem Proving, in order to develop new
methodologies for handling quantitative properties related to program
resource consumption, like execution time and space. The task of
verifying and certifying quantitative properties is undecidable as
soon as the considered programming language gets close to a general
purpose language. So, full-automatic techniques in general cannot help
in classifying programs in a precise way with respect to the amount
of resources used and moreover in several cases the programmer will
not gain any relevant information on his programs. In particular,
this is the case for all the techniques based on the study of structural
constraints on the shape of programs, like many of those actually
proposed in the field of implicit computational complexity. To overcome
these limitations, we aim at combining the ideas developed in the linear
logic approach to implicit computational complexity with the ones of
interactive theorem proving, getting rid of the intrinsic limitations
of the automatic techniques.

HOW TO APPLY:
All candidates are invited to send by email the following material to Ugo
Dal Lago (dallago at cs.unibo.it), before May 31st, 2011:
- A detailed CV;
- A short statement about the candidate's motivation for working
   in the "ETERNAL" project;
- An abstract of the candidate's Ph.D. thesis (if already discussed).
- Letters of recommendation (if any).
For any further information, please write to dallago at cs.unibo.it
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20110510/505e69fc/attachment.html>