[TYPES/announce] PhD position in programming languages and formal proof

[Randy Pollack]

[ The Types Forum (announcements only), 
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


  Certified Complexity Preserving Compiler (CerCo):
  Programming and proving a compiler in Type Theory

For details contact Randy Pollack rpoll...@inf.ed.ac.uk.

** This is restricted to EU students. **

A 3 year PhD studentship is available in a project titled A Certified
Complexity Preserving Compiler (CerCo), funded by the European
Commission under Future and Emerging Technologies (FET).

The studentship will be held within the Laboratory for Foundations of
Computer Science, at the School of Informatics, University of
Edinburgh, to begin in 2010, start date flexible.

The CerCo project aims at the construction of a formally verified
complexity preserving compiler from a large subset of the C
programming language to some typical micro-controller assembly
language of the kind used in embedded systems. The work comprises the
definition of cost models for the input and target languages, coding
the compiler in Type Theory and the machine-checked proof of
preservation of complexity (concrete, not asymptotic) along
compilation, using the *Matita* proof tool. The compiler will return
certified cost annotations for the source program, providing a
reliable infrastructure to draw temporal assertions on the executable
code while reasoning on the source. The compiler will be open source,
and all proofs will be public domain.

The permanent researchers involved in the CerCo project are Randy
Pollack in Edinburgh, Andrea Asperti and Claudio Sacerdoti-Coen in
Bologna and Roberto Amadio and Yann Regis-Gianas in Paris. The
Edinburgh site will focus on the compiler front end. We are interested
in use of dependent types in programming as well as in proof.

Suitable candidates will have a strong first degree in Computer
Science and a strong interest in formal proof and type theory.

Candidates are encouraged to contact Randy Pollack to informally
discuss the project further. Formal application will be through the
School's normal PhD application process:
http://www.inf.ed.ac.uk/postgraduate/phd.html

--
Randy Pollack
Phone: +44 131 650 5145  URL: http://homepages.inf.ed.ac.uk/rpollack
Edinburgh University, Informatics Forum, 10 Crichton Street, Edinburgh EH8 9AB

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[TYPES/announce] Workshop Realizability in Cham béry

[Pierre Hyvernat]

[ The Types Forum (announcements only), 
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Greetings to all!

This is the first official announcement for the third workshop
Réalisabilité à Chambéry.

This year's workshop will take place during week 22, that is Tuesday
1st of June -- Friday 4th of June.

If enough participants express interest for it, Monday the 31st of May
will be used for a preliminary course before the actual workshop.


Partial information can already be found on the web page:
  http://www.lama.univ-savoie.fr/~hyvernat/Realisabilite2010/
and you can register for the workshop there:
  
http://www.lama.univ-savoie.fr/~hyvernat/Realisabilite2010/index.php?page=registration


There will be an invited course given by Martin Hyland as well as two
invited seminars by Thomas Streicher and Jaap van Oosten.

There will be 2 sessions for contributed talks, and PhD students are
particularly encouraged to submit a talk. (There will be no official
proceedings though.)


More details about contents of invited talks and schedule will be added
to the web page when available.

Meanwhile, feel free to register (via the web page), submit talks or
contact me for additional details (or comments).


Note: the workshop will be similar in spirit to the last one.  The
intention is to have a nice and friendly week without all the glitter of
big conferences.  There is no registration fee, but the organizing
committee doesn't organize much besides the actual workshop.

There is a possibility to get a student room (on campus, very cheap, but
only a bare room).  Students will of course be given priority for those,
but anyone can ask for one...
Other possibilities for accommodation are given on the web page:
  
http://www.lama.univ-savoie.fr/~hyvernat/Realisabilite2010/index.php?page=location



Pierre Hyvernat
-- 
I don't quite hear what you say, but I beg to differ
entirely with you.
-- Augustus De Morgan