[No longer available]
Context
The Abella theorem prover is an interactive prover that has been designed for inductive and co-inductive reasoning over syntax containing bindings. It makes use of a two-levels of logic where one logic is used to specify computation (a la logic programming and SOS specifications) and a second logic for reasoning about such specifications. Some of its most distinctive applications have been to proving meta-theoretic properties of the lambda-calculus and the pi-calculus. The implementation of Abella has been a cooperative project between the Parsifal team at INRIA Saclay and the University of Minnesota. Many others have helped contribute to the logic underlying the system and to the design and applications of the prover.
Experience with example specifications and strong reasoning principles (such as those behind logical relations and Howe’s method) require making extensions to the underlying logic of Abella and/or to its design. Such extensions are those related to adding higher-order (predicate) quantifications, polymorphic types, and broader uses of the nabla quantifier. Different choices of specification logic (such as linear logic) are also desirable for some applications.
Mission
The goal of this postdoc is to propose and study various extensions to the logic underlying Abella and to the design and methodology of Abella for addressing the system’s current limitations in expressiveness. Proof theoretic techniques have proved the most valuable in this setting.
Description of work
The postdoc will work with the current literature involving the proof theory of fixed points, higher-order abstract syntax, and the nabla-quantifier. Experience using Abella has shown that there are a number of extensions that need to be considered to both the underlying logic and the implemented system in order to continue to capture specification and reasoning tasks in their most declarative and natural setting.
An engineer/programmer is associated with the team so some support is available within the team for system building.
Skills and Profile
The successful candidate should have a strong background in computational logic generally. Particular needs include: a basic background in sequent calculus and the lambda-calculus; familiarity with structured operational semantics; and programming skills in high-level languages such as ML, OCaml, Prolog, and lambda Prolog.
Application Details
The position is an INRIA PostDoc position and the candidate must fulfill the formal requirements. 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 defence date and the composition of the thesis committee.
To apply, please contact Dale Miller (dale.miller@inria.fr) before 5 March 6 June 2012. Please include a CV with your mail. Candidates will also be required to make a formal application on INRIA’s web-site: instructions will be provided via e-mail.
The position will be at the Laboratoire d’Informatique (LIX) in the École Polytechnique, situated to the south of Paris. French proficiency is not necessary.
