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

TU Delft as an employer

You will be based at TU Delft in the Programming Languages group and work within a strong international research environment as part of a collaboration spanning five Dutch universities.

Conditions of employment

• Duration of contract is 2 years Temporary
• 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.