Do not wait for the deadline: applications will be treated on the fly.
Application deadline: 29 October 2017
PhD start deadline: 1st January 2018
Summary: To widen their use, proof assistants needs more automation. This can be performed by calling external automated theorem provers. Centered around Dedukti, a proof checker for the universal logical framework λΠ-calculus modulo theory, the objective is to design a proof environment that is able to call external provers to build part of the proof. The global architecture must emphasize the need to have a correct and exhaustive proof once the portions proved externally are glued together. From Dedukti to external provers, proof obligations in the λΠ-calculus modulo theory must be passed in an efficient way, either by encoding them or by extending the external prover to accept them. Reciprocally, proofs or proof traces produced by these tools needs to be reconstructed back into Dedukti.
Place: Laboratory on Specification and Verification (LSV) from the University Paris Saclay
Supervisors: Frédéric Blanqui and Guillaume Burel
Eligibility: candidates should hold a master degree or equivalent diploma in logic or computer science with some background in proof theory
Funding: net about 1661 euros/month for 3 years (including social security)
How to apply: send a CV and motivation letter by email to the supervisors
More details available here.