THIS POSITION HAS BEEN FILLED
Context
The ANR/FWF project STRUCTURAL investigates the structural and computational proof theory of recent proof formalisms such as deep inference and proof-nets. One of its main goals is to find canonical proof objects that are also suitable for computation in terms of proof search and normalization. Traditional proof systems such as the sequent calculus, although well-suited for search, do not yield canonical proofs because their syntax records irrelevant details such as a particular but arbitrary order for permutable rules. More “bureaucracy-free” formalisms such as proof-nets can have represent the parallelism in a proof graphically and therefore canonically, but such formalisms are generally only well behaved on logics with a low expressive power. Recent results using deep inference and focusing suggest interesting future directions for this research goal. More details of the research effort can be found in the scientific programme of the STRUCTURAL project.
Position
This is a call for a post doctoral position to support the research effort and goals expressed in the scientific programme within the INRIA Parsifal team. The successful candidate will undertake basic research in the design of new proof systems that both provide canonical proof objects and are concrete enough structures to support the computational aspects of proof search and normalization.
General Information
- Duration: 12 months
- Starting date: Fall 2012 (between 1 Sep and 1 Nov)
- Location: Laboratoire d’Informatique (LIX), Ecole Polytechnique
- Application Deadline: 20 May, 2012
Requirements
Candidates must have a Ph.D. and a strong background in proof theory and related fields. If the Ph.D. thesis is not yet defended, the candidate must provide the planned defence date and the composition of the thesis committee.
To apply, please contact both the following people as soon as possible. Include your current CV, a link to a list of your publications, and a research statement summarizing your research activities and goals.
- Kaustuv CHAUDHURI
(kaustuv.chaudhuri@inria.fr) - Lutz STRASSBURGER
(lutz at lix dot polytechnique dot fr)
Please also include the names of two references.
The deadline for applications is 20 May 2012, but early expression of interest is encouraged.
More Information
- The STRUCTURAL project
- The STRUCTURAL project description (PDF)
- LIX / École Polytechnique is situated to the south of Paris, directly on the RER-B regional rail line. The position will be in the newly built Digiteo building on the Polytechnique campus.
