[TYPES/announce] possible INRIA post doc in mechanizing meta-theory

[Dale Miller]

As part of INRIA's 2009 campaign for recruiting postdocs, the Parsifal
team is looking to hire someone on the following topic:

Mechanizing the meta-theory of programming and logics

Research Context:
Inference rules are commonly used in the specification of the dynamic
and static semantics of programming languages: in particular, both
structural operational semantics and typing are commonly defined via
inference rules over relational judgments.  Traditional approaches to
reasoning about such specifications first encode them into a
functional or denotational setting and then reason with the encodings
via theorem provers designed for (constructive) mathematics.  The
Parsifal team has been developing an alternative approach to reasoning
about such specifications that does not encode them: instead,
reasoning is done directly on the relational specifications.  Many of
the intensions aspects of computation, such as bound variables and
resources, can then be handled directly using basic notions from proof
theory.

Activities for the Post Doc:
The postdoc will work with prototype interactive and automatic provers
currently underdevelopment within the team and their colleagues (see
links below).  These provers range from model checkers to general
purpose theorem provers for logics that involve induction,
coinduction, and elements of higher-order quantification.  The postdoc
will be expected to develop sizable examples within the general area
of mechanized meta-theory, to help in justifying or redesigning the
meta-logics, and to construct a comprehensive methodology for dealing
with mechanized meta-theory.

Required knowledge and background:
Computational logic; basic background in sequent calculus and
lambda-calculus; and programming skills in high-level languages such
as ML, OCaml, Prolog, and lambda Prolog.  For more specifics on the
prototype systems mentioned above, see:
    http://slimmer.gforge.inria.fr/bedwyr/
    http://slimmer.gforge.inria.fr/tac/
    http://abella.cs.umn.edu/

Further particulars:
Duration: 12 month
Starting date: Between 1 Oct 2009 and 1 Dec 2009
Working place: Ecole Polytechnique, LIX, Equipe Parsifal

The position is an INRIA-postdoc position and candidate must fulfill
the formal requirements found at
http://www.inria.fr/travailler/opportunites/postdoc/postdoc.en.html.
In particular, the candidate must have held a doctorate or Ph.D. for
less than one year before the recruitment date.  If the Ph.D. is not
defended at the application date, you should clearly point out the
defense date and the composition of thesis jury.

Applications should be made via this web site and by sending all
application material also to Dale Miller (dale at
lix.polytechnique.fr) before 22 May 2009.  (Late applications may also
be considered if the position is not filled.)

See also: http://www.lix.polytechnique.fr/parsifal/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20090309/a959ebbd/attachment-0001.htm