Funded PhD studentship: Integrating Automated Provers in Proof Assistants

be careful 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.

Statcounter W3C Validator Last updated on 4 July 2017. Come back to main page.