Post-Doc position in the CerCo FET-Open EU Project

Post-Doc position in the CerCo FET-Open EU Project

[Claudio Sacerdoti Coen]

Job description:

We are currently looking for a Post-Doc position at the Department of
Computer Science, University of Bologna, to work on the CerCo FET-Open
EU Project (see description below). The gross salary is 36000 euros per
year. The University of Bologna is the oldest western university and the
Department of Computer Science (http://www.cs.unibo.it/en/), located in
the historic city center, has strong expertise in theoretical computer
science and logic and it participates to several national and
international projects. The Post-Doc will join the HELM team, leaded by
Prof. Asperti, whose members work in the domains of Type Theory and
Mathematical Knowledge Management. The CerCo project is headed by
Dr. Sacerdoti Coen. The candidate will benefit from exchange opportunity
with the other project participants (University Paris-Diderot, Paris,
and University of Edinburgh, Edinburgh). The candidate will not have any
teaching duties.

Requirements:

Candidates should have a Ph.D. in Computer Science and previous
experience in either Type Theory (in particular Interactive Theorem
Proving) or Compiler Development, and being proficient in functional
programming languages.

Starting date:

The starting date will be decided together with the candidate and could
not be before March. The contract is for two years. The candidate should
contact sacerdot@cs.unibo.it for further information.

Project description:

The CerCo FET-Open EU Project is aimed at producing the first _formally_
_verified_ _complexity_preserving_ compiler for a subset of C to the
object code for a microprocessor used in embedded systems. The output of
the compilation process will be the object code and a copy of the source
code annotated with _exact_ computational complexities for each program
slice in O(1). The exact computational complexities (expressed in clock
cycles and parametric in the program input) can then be used to formally
reason on the overall code complexity. The source code of the compiler
will be formally verified using the Matita Interactive Theorem Prover
(http://matita.cs.unibo.it), based on a variant of the Calculus of
(Co)Inductive Constructions.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: sacerdot@cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------

PhD student in the FormMath project

[Herman Geuvers]

Job description
The aim of the FORMATH project(http://www.formath.cs.ru.nl) is to
develop libraries of formalized mathematics concerning algebra, linear
algebra, real number computation, and algebraic topology:
These libraries will be structured as software components, relying on
Ssreflect, which has proved its worth in the formal proof of the four
colour theorem, and to address topics that were mostly left untouched
by previous research in formal proofs or formal methods.

This work concerns formally proved algorithms for solving problems in
real arithmetics, solving problems in ordinary differential equations,
or solving problems in algebraic topology.
Our methodology is a combination of theoretical research and
technological development. The main tools will be provided by the
Mathematical Components project, for instance the Ssreflect library
for Coq proof assistants.

The four partners in the EU ForMath project are:
- Goteborg;
- INRIA;
- Nijmegen;
- La Roja.

More specifically, as a PhD student at the Nijmegen location you will
work on Work package 4;
- Real number computation and basic numerical analysis;
- The use of exact real number computation to prove inequalities.

The objective is specification and implementation of a simple ODE
solver. Potential fields of applications include robotics and hybrid
systems.

Requirements
You should meet the following requirements:
- A master's degree (or equivalent) in Computer Science, Mathematics
or a related field, with a strong interest in proof assistants, type
theory, functional programming, constructive analysis and numerical
analysis;
- Commitment and a cooperative attitude;
- Excellent proficiency in written and spoken English.

Organization
The Radboud University Nijmegen is one of the leading academic
communities in the Netherlands. Renowned for its green campus, modern
buildings, and state-of-the-art equipment, it has nine faculties and
enrols over 17.500 students in approximately 90 study programmes. The
university is situated in the oldest Dutch city, close to the German
border, on the banks of the river Waal (a branch of the Rhine). The
city has a rich history and one of the liveliest city centres in the
Netherlands.
The section Intelligent Systems of the Institute for Computing and
Information Sciences (ICIS) at the Radboud University Nijmegen studies
mathematical theories concerned with computability, provability and
complexity. Notably, the group studies type theory, lambda calculus
and logic and also applies these theories in the area of theorem
proving and formalizing mathematics.
The group has an excellent international reputation which was
supported by the last national research assessment.
Website: http://www.cs.ru.nl

Conditions of employment
Employment: 1,0 fte
Maximum salary per month, based on a fulltime employment: € 2,612 gross/month
Starting at € 2,042 per month, the salary will increase to € 2,612 per
month in the fourth year.
PhD scale.

Additional conditions of employment
You will be appointed as a PhD student for a period of four years.
Your performance will be evaluated after 18 months. If the evaluation
is positive, the contract will be extended by 2.5 years.

Additional Information
Bas Spitters
Telephone: +31 24 3652611
E-mail: spitters@cs.ru.nl
Telephone: +31 24 3652104

Application
You can apply for the job (mention the vacancy number 62.52.09) before
1 February 2010 by sending your application -preferably by email- to:

RU Nijmegen, FNWI, P&O, mrs. D. Reinders
P.O. Box 9010, 6500 GL Nijmegen, NL
Telephone: +31 24 3652027
E-mail: pz@science.ru.nl
http://www.ru.nl/vacaturedetails?recid=497982

[Caml-list] Post-Doc positions in the CerCo FET-Open EU Project

[Claudio Sacerdoti Coen]

=== Two New Post-Doc positions in the CerCo FET-Open EU Project ===

** Job duration: 01/07/2012-30/06/2013 (one year)
** Deadline for reception of candidatures: 29/06/2011

We are currently looking for two Post-Doc positions at the Department of
Computer Science, University of Bologna, to work on the CerCo FET-Open
EU Project (see description below). The gross salary is 26174 euros per
year. Only a minimal amount of taxes is due.

The University of Bologna is the oldest running western university and the
Department of Computer Science (http://www.cs.unibo.it/en/), located in
the historic city center, has strong expertise in theoretical computer
science and logic and it participates to several national and
international projects. The Post-Doc will join the HELM team, leaded by
Prof. Asperti, whose members work in the domains of Type Theory and
Mathematical Knowledge Management. The CerCo project is headed by
Dr. Sacerdoti Coen. The candidates will benefit from exchange opportunity
with the other project participants (University Paris-Diderot, Paris,
and University of Edinburgh, Edinburgh). The candidates will not have any
teaching duties.

Requirements:

We are looking for candidates with a Ph.D. in Computer Science and
previous experience in Type Theory (in particular Interactive
Theorem Proving), and being proficient in functional programming languages.
We also accept candidates that will defend their Ph.D. thesis in the near
future, if they can provide a formal proof that they will.

Starting date:

The proposed starting date is the 01/07/2012. The contract is for one
year. The candidate should contact sacerdot@cs.unibo.it for further
information.

Project description:

The CerCo FET-Open EU Project is aimed at producing the first _formally_
_verified_ _complexity_preserving_ compiler for a subset of C to the
object code for a microprocessor used in embedded systems. The output of
the compilation process will be the object code and a copy of the source
code annotated with _exact_ computational complexities for each program
slice in O(1). The exact computational complexities (expressed in clock
cycles and parametric in the program input) can then be used to formally
reason on the overall code complexity. The source code of the compiler
will be formally verified using the Matita Interactive Theorem Prover
(http://matita.cs.unibo.it), based on a variant of the Calculus of
(Co)Inductive Constructions. The candidate will contribute to the formal
proof of correctness of the compiler.

How to submit candidatures:

All candidates are invited to get in touch in advance with Dr. Claudio
Sacerdoti Coen <sacerdot@cs.unibo.it>, submitting a curriculum vitae.

The official candidature must be received by standard mail (no
electronic submission) before the 29/06/2011. Candidates must fill in the
forms (in Italian only) that can be found at the following address:

https://www.aric.unibo.it/AssegniRicerca/BandiPubblicati/zz_Bandi_din.aspx
(look for the word "Matita" in the second column)

Candidates must also attach two recommendation letters.

Foreign candidates will be helped in compiling the forms.

					Kind regards,
					  C.S.C.


-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: sacerdot@cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------