Lean for Program Verification with MLIR

Stream: job postings

[Tobias Grosser]

We just opened a position at the University of Edinburgh to use lean in connection with compilers:

We are researching innovations in formal methods to reduce the verification cost of production compilers. We will evolve the Lean4 ecosystem by improving the lean mathlibrary mathlib, lean’s tactic framework, and lean itself with the objective to streamline formal verification of compilers and programming languages. We will then use this technology to formally verify the foundations of the MLIR compiler stack.

You may know @Siddharth Bhat and @Chris Hughes from my group already. We just recently upstreamed the lean LLVM backend (https://github.com/leanprover/lean4/pull/1837), contribute to porting mathlib, wrote a lean MLIR backend (https://grosser.science/pub/bhat22lambda) and play with formal semantics for MLIR (https://github.com/opencompl/lean-mlir).

https://elxw.fa.em3.oraclecloud.com/hcmUI/CandidateExperience/en/sites/CX_1001/job/6208/?utm_medium=jobshare

Drop me a line at tobias.grosser@ed.ac.uk if you need further information. (Also, if you are interested in a post-doc let me know. Such a position might also be possible).

[Patrick Massot]

Is that a permanent position?

[Kevin Buzzard]

It looks like it's 24 months according to the link

[Tobias Grosser]

Indeed, it's a 24 months position.

[Patrick Massot]

Then what is the difference with a post-doc?

[Andrés Goens]

From the description, it seems that the position doesn't require a doctorate:

Undergraduate Degree in Computer Science or Mathematics

Patrick Massot said:

Then what is the difference with a post-doc?

[Andrés Goens]

(for reference, they also call PhD students "postgraduate students" here)

[Patrick Massot]

Oh! I see. It didn't cross my mind that a job could not require a PhD, that's why I was so confused.

[Tobias Grosser]

It can, but it is not a necessity.