From: Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>
To: spitters@cs.ru.nl, types-announce@lists.seas.upenn.edu,
types@lists.chalmers.se, fm-announcements@lists.nasa.gov,
caml-list@inria.fr, grin@di.unipi.it
Cc: isabelle-users@cl.cam.ac.uk, formal-methods@cs.uidaho.edu,
coq-club@pauillac.inria.fr, acl2@cs.utexas.edu,
chiarabi@mathematik.uni-muenchen.de
Subject: Post-Doc position in the CerCo FET-Open EU Project
Date: Tue, 05 Jan 2010 12:15:07 +0100 [thread overview]
Message-ID: <1262690107.5919.57.camel@zenone> (raw)
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
----------------------------------------------------------------
next reply other threads:[~2010-01-05 11:06 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-01-05 11:15 Claudio Sacerdoti Coen [this message]
2010-01-06 15:11 ` PhD student in the FormMath project Herman Geuvers
[not found] ` <1296059286.27942.41.camel@zenone>
2012-06-01 2:57 ` [Caml-list] Post-Doc positions in the CerCo FET-Open EU Project Claudio Sacerdoti Coen
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=1262690107.5919.57.camel@zenone \
--to=sacerdot@cs.unibo.it \
--cc=acl2@cs.utexas.edu \
--cc=caml-list@inria.fr \
--cc=chiarabi@mathematik.uni-muenchen.de \
--cc=coq-club@pauillac.inria.fr \
--cc=fm-announcements@lists.nasa.gov \
--cc=formal-methods@cs.uidaho.edu \
--cc=grin@di.unipi.it \
--cc=isabelle-users@cl.cam.ac.uk \
--cc=spitters@cs.ru.nl \
--cc=types-announce@lists.seas.upenn.edu \
--cc=types@lists.chalmers.se \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox