Postdoc Cyclic Programming and Reasoning

Help us build the next generation of verification tools by bringing cutting-edge proof assistant technology to bear on real-world Rust programs.    

Job description

Software is at the core of modern society — from communication networks and financial systems to medical devices and transport infrastructure — and ensuring that it behaves correctly is both essential and notoriously difficult. Proof assistants such as Agda and Rocq (formerly Coq) make it possible to construct mathematically rigorous, machine-checked guarantees about software behaviour, but applying them to programs written in mainstream languages remains a significant challenge. This is especially true for software that exhibits cyclic behaviour: programs with loops, recursive data, or continuous interaction with their environment, which require a careful interplay of inductive and coinductive reasoning to verify.

In this postdoc position, you will work at the intersection of proof assistants and modern systems programming. Your central task is to design and prototype a way to verify Rust programs — and in particular programs with cyclic structures — by translating them, together with logical annotations supplied by the developer, into a proof assistant where their correctness can be machine-checked. The aim is not to build yet another verification tool from scratch, but to make state-of-the-art research on inductive-coinductive type theory genuinely usable for Rust developers. You will work closely with a parallel PhD project on first-class coinduction in proof assistants, helping to refine the underlying type theory and putting it to the test on realistic Rust programs.

This position is part of the NWO-XL consortium project Cyclic Structures in Programs and Proofs: New Harmonies in Software Correctness by Construction, a collaboration between five Dutch universities (TU Delft, Groningen, Leiden, Nijmegen, and Twente) which brings together expertise in formal logic, programming language theory, concurrency, and proof assistants. You will be based at TU Delft in the Programming Languages group, supervised by Jesper Cockx, and will collaborate closely with the other PhD students, postdocs, and senior researchers in the consortium. Within the wider project, your work forms a bridge between foundational research on coinductive reasoning and its practical application to real programs, and as such will play a key role in demonstrating that the consortium's theoretical advances translate into concrete tools that practitioners can use.

You will have significant freedom to shape the technical agenda, publish your findings at leading venues (such as POPL, ICFP, OOPSLA, ITP, and CPP), and contribute to the open-source tools developed within the consortium. You will also be encouraged to spend time at one of the partner universities and to engage with the broader national and international research community via the NetTCS network and consortium-organised workshops and schools.   

Job requirements 

• A PhD in computer science, mathematics, or a closely related discipline (obtained or expected to be obtained before the starting date)
• Solid experience using a proof assistant such as Agda, Rocq, or Lean, ideally for non-trivial formalisations or for research on the proof assistant itself
• A strong background in type theory and/or programming language theory, including familiarity with topics such as dependent types, type systems for program verification, or operational/denotational semantics
• The ability to conduct independent research, demonstrated by peer-reviewed publications at relevant international venues
• Good written and spoken English, and the communication skills needed to collaborate effectively within a multi-site consortium   

Conditions of employment 

• Duration of contract is 2 years Temporary
• A job of 36-40 hours per week. 
• Salary and benefits are in accordance with the Collective Labour Agreement for Dutch Universities.
• An excellent pension scheme via the ABP. 
• The possibility to compile an individual employment package every year. 
• Discount with health insurers on supplemental packages. 
• Flexible working week. 
• Every year, 232 leave hours (at 38 hours). You can also sell or buy additional leave hours via the individual choice budget. 
• Plenty of opportunities for education, training and courses. 
• Partially paid parental leave 
• Attention for working healthy and energetically with the vitality program. 

Will you need to relocate to the Netherlands for this job? TU Delft is committed to make your move as smooth as possible! The HR unit, Coming to Delft Service, offers information on their website to help you prepare your relocation. In addition, Coming to Delft Service organises events to help you settle in the Netherlands, and expand your (social) network in Delft. A Dual Career Programme is available, to support your accompanying partner with their job search in the Netherlands.  . 

Additional information
If you would like more information about this vacancy or the selection procedure, please contact Jesper Cockx, via J.G.H.Cockx@tudelft.nl.

Application procedure
Are you interested in this vacancy? Please apply no later than 1 July 2026 via the application button and upload the following documents:

• CV
• Motivational letter

You can address your application to Jesper Cockx.

Please note:

• You can apply online. We will not process applications sent by email and/or post. 
• As part of knowledge security, TU Delft conducts a risk assessment during the recruitment of personnel. We do this, among other things, to prevent the unwanted transfer of sensitive knowledge and technology. The assessment is based on information provided by the candidates themselves, such as their motivation letter and CV, and takes place at the final stages of the selection process. When the outcome of the assessment is negative, the candidate will be informed. The processing of personal data in the context of the risk assessment is carried out on the legal basis of the GDPR: performing a public task in the public interest. You can find more information about this assessment on our website about knowledge security.
• Please do not contact us for unsolicited services.