Postdoc position to the Computing Science division

Join the CakeML research project and be part of developing new verified compilers and proved-to-be-correct programming language implementations. The CakeML project is a friendly, highly collaborative, open source effort, which spans several countries and institutions.


Project description
This postdoc position is part of a grant (from the Swedish Research Council) on making new verified compilers based on the verified CakeML compiler. Early results include the verified PureCake compiler for a Haskell-like source language [PLDI 2023] and the verified Pancake compiler for a low-level programming language [PLOS 2023]. The project itself is quite open ended, but the overall aim is to build new verified compilers based on (parts of) the CakeML compiler.

My group is part of the Formal Methods unit within the Computing Science division at the Computer Science and Engineering department of Chalmers university. The unit and the broader division are lively environments with fun interactions between research areas such as functional programming, formalised mathematics, type theory, information security and more.


Major responsibilities
The research part of the position (80 %) will focus on the grant mentioned above. This work involves developing new verified compilers, improving existing ones, and developing case studies that showcase the verified compilers. Since the CakeML compiler is developed in the HOL4 interactive theorem prover, HOL4 is the tool that is most likely to be used. However, there may be opportunities to broaden the reach of CakeML to other interactive theorem provers and thus there is space to use other tools too.


The teaching part of the position (20 %) will consist of helping with courses the department offers. The teaching duties can range from being a teaching assistant, supervising MSc projects, or even lecturing a course.

Qualifications
To qualify for the position of postdoc, you must:

- Have a PhD in Computer Science, Mathematics, Logic or Philosophy. The doctoral degree must be awarded no more than three years prior to the application deadline (according to the current agreement with the Swedish Agency for Government Employers). Exceptions from the 3-year limit can be granted for parental leave, sick leave, or military service.

- Have significant experience in use and/or development of interactive theorem provers, such as HOL4, Isabelle/HOL, HOL Light, Lean, Coq, ACL2 or similar.

- Have past experience in research on programming languages, compilers or verified proof checkers.

- Have sound verbal and written communication skills in English

Prior experience of tools in the HOL family of interactive theorem provers is a plus.

You are expected to be somewhat accustomed to teaching, and to demonstrate good potential within research and education.

Swedish is not a requirement but Chalmers offers Swedish courses.

Contract terms
This postdoc position is a full-time temporary employment for two/three years.

We offer
Chalmers offers a cultivating and inspiring working environment in the coastal city of Gothenburg. 
Read more about working at Chalmers and our benefits for employees.

Chalmers aims to actively improve our gender balance. We work broadly with equality projects, for example the GENIE Initiative on gender equality for excellence. Equality and diversity are substantial foundations in all activities at Chalmers.

Application procedure
The application should be marked with 20240058 and written in English. The application should be sent electronically and be attached as PDF-files, as below. Maximum size for each file is 40 MB. Please note that the system does not support Zip files.

CV: (Please name the document as: CV, Surname, Ref. number) including:
• CV, include complete list of publications
• Previous teaching and pedagogical experiences
• Two references that we can contact.

Personal letter: (Please name the document as: Personal letter, Family name, Ref. number)
1-3 pages where you:
• Introduce yourself
• Describe your previous research fields and main research results
• Describe your future goals and future research focus

Other documents:
• Attested copies of completed education, grades and other certificates.

Use the button at the foot of the page to reach the application form.

Application deadline: 5, March, 2024

 
For questions, please contact:
Prof, Magnus Myreen, CS, myreen@chalmers.se, 0729744943


*** Chalmers declines to consider all offers of further announcement publishing or other types of support for the recruiting process in connection with this position. *** 





Chalmers University of Technology conducts research and education in engineering sciences, architecture, technology-related mathematical sciences, natural and nautical sciences, working in close collaboration with industry and society. The strategy for scientific excellence focuses on our six Areas of Advance; Energy, Health Engineering, Information and Communication Technology, Materials Science, Production and Transport. The aim is to make an active contribution to a sustainable future using the basic sciences as a foundation and innovation and entrepreneurship as the central driving forces. Chalmers has around 11,000 students and 3,000 employees. New knowledge and improved technology have characterised Chalmers since its foundation in 1829, completely in accordance with the will of William Chalmers and his motto: Avancez!