[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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/