Research Assistant/Research Associate: The Department of Computer Science and Technology at the University of Cambridge, UK, is seeking a Research Assistant or Research Associate (PostDoc) to join the Compiler Lab team. This role involves working on the development of formally verified compiler infrastructure to enhance the LLVM/MLIR compiler ecosystem.
Research Assistant/Research Associate in Compiler Lab
Designation:
Research Assistant or Research Associate (PostDoc)
Research Area:
Compiler Infrastructure Development with a focus on formally verified compilation
Location:
Department of Computer Science and Technology, University of Cambridge, UK
Eligibility/Qualification:
- Research Associate: PhD in Computer Science or equivalent experience in compiler design and interactive theorem proving, with relevant scientific publications.
- Research Assistant: Master’s in Computer Science or equivalent experience.
Job Description:
The successful candidate will collaborate with a team of students and research collaborators to advance the formal verification of compiler technology. This role involves contributing to various aspects of the Lean4 proof assistant, such as developing a powerful BitVector library, coinductive proofs, integrating MLIR’s SSA data structures into Lean, and modeling instruction-set level semantics. The appointed individual will engage in large-scale open-source software development and have the opportunity to explore automation techniques for superoptimization, enhancements in interactive-theorem-prover-based verification, and other innovative avenues towards the team’s objectives.
How to Apply:
Interested candidates can apply online by clicking the ‘Apply’ button on the recruitment system of the Department of Computer Science and Technology, University of Cambridge. For additional information, applicants can contact Tobias Grosser via his website at http://www.grosser.science. When applying, please reference NR42806 in the application and any related correspondence.
Closing Date for Application:
18 August 2024
This job post emphasizes the opportunity for researchers to contribute to cutting-edge work in compiler technology within a collaborative academic environment at the University of Cambridge.
