From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p5KJm6N1014736 for ; Mon, 20 Jun 2011 21:48:06 +0200 X-IronPort-AV: E=Sophos;i="4.65,396,1304287200"; d="scan'208";a="97130481" Received: from mail-qy0-f182.google.com ([209.85.216.182]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 20 Jun 2011 21:48:01 +0200 Received: by qyk38 with SMTP id 38so1238366qyk.6 for ; Mon, 20 Jun 2011 12:48:00 -0700 (PDT) MIME-Version: 1.0 Received: by 10.229.215.6 with SMTP id hc6mr700979qcb.93.1308599280064; Mon, 20 Jun 2011 12:48:00 -0700 (PDT) Received: by 10.229.214.6 with HTTP; Mon, 20 Jun 2011 12:48:00 -0700 (PDT) Date: Mon, 20 Jun 2011 21:48:00 +0200 Message-ID: From: Kaustuv Chaudhuri To: caml-list@inria.fr Content-Type: text/plain; charset=UTF-8 Subject: [Caml-list] Junior engineer position at INRIA Saclay/Ecole Polytechnique, France The Parsifal research team at INRIA Saclay and the Ecole Polytechnique has an open call for one junior engineer position (2 years). The main task of the recruited engineer will be to work on the integration and further development of a number of computational logic systems designed and built by the team members in recent years. Some tasks involved are: - Designing and implementing a common formal framework for communication between the Abella proof assistant, the Bedwyr symbolic model checker, and the Tac inductive theorem prover. - Using the Teyjus implementation of the Lambda Prolog programming language to represent and animate logical specifications of deductive and computational systems. - Investigating a number of application domains including the formal meta-theory of computational systems (programming languages, process calculi, etc.), and the use of formal proofs as certificates (eg. proof-carrying code, marketplace of proofs). Candidates should have a bachelor's degree in computer science, be familiar with the OCaml programming language (or similar high-level programming languages), and have a background in logic, formal methods, and symbolic computing. As this engineer will work with a team of international researchers, the candidate should be fluent in English. Knowledge of French is desirable but not mandatory. The position should begin in October 2011. Interested candidates are encouraged to contact the following people: Dale Miller . Kaustuv Chaudhuri Some links: Official announcements: http://www.lix.polytechnique.fr/parsifal/dokuwiki/doku.php?id=engineer http://en.inria.fr/institute/recruitment/offers/young-graduate-engineers Parsifal team web page: http://www.lix.polytechnique.fr/parsifal/ System descriptions: Bedwyr http://slimmer.gforge.inria.fr/bedwyr/ Abella http://abella.cs.umn.edu/ Tac http://slimmer.gforge.inria.fr/tac/ Teyjus http://teyjus.cs.umn.edu/