PhD grant available on function & type equivalences in Lean

Stream: job postings

[Frédéric Blanqui]

Context: Proof systems, automated or interactive, have increasing applications in education, industry and research. Although interoperability is a very important property in engineering and computer science to reduce development costs, it is poorly developed within proof systems. This greatly hinders the democratization of those tools and the formalization of advanced mathematical results. One way to improve interoperability is to develop translations between systems. But for translated definitions and theorems to be readily usable, the translated types and functions must be aligned with those already used in the target systems. To this end, it is necessary to prove that a type or a function can be substituted by another one. However, for this to be correct, one needs to show that the two types are indeed isomorphic and that the two functions are indeed equal. This project aims at developing tools to automate this kind of proofs as much as possible.

Goal: The goal of this project is to make the existing translations of libraries of mathematical definitions and proofs from one system to the other directly usable by the users of the target systems, by proving the equivalence of the various definitions of the same mathematical notions, and developing proof tactics to automate those proofs as much as possible. As a concrete benchmark, the candidate will start by the translation in Lean of the HOL-Light library on real and complex analysis, which contains more than 20,000 theorems.

Place: Deducteam, LMF, ENS Paris Saclay, France

Supervisors: Frédéric Blanqui and Patrick Massot

Find more details on https://blanqui.gitlabpages.inria.fr/equiv.html.

Application deadline: July 27.

For any question, please contact me.

[Notification Bot]

This topic was moved here from #announce > PhD grant available on function or type equivalence in Lean by Mario Carneiro.