Jobid=623070806273893262 (0.0199)
ph3Postdoc Cyclic Programming and Reasoning /h3 pbHelp us build the next generation of verification tools by bringing cutting‑edge proof assistant technology to bear on real‑world Rust programs. /b /p pSoftware 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 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. /p pIn 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. /p pThis 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. You will be based at TU Delft in the Programming Languages group, supervised by Jesper Cockx, and will collaborate closely with the consortium’s PhD students, postdocs and senior researchers. /p h3Responsibilities /h3 ul liDesign and prototype verification of Rust programs with cyclic structures. /li liTranslate Rust code and developer‑supplied annotations into a proof assistant for machine checking. /li liCollaborate with a parallel PhD project to refine coinductive type theory and evaluate it on realistic Rust programs. /li liPublish findings at leading venues such as POPL, ICFP, OOPSLA, ITP and CPP. /li liContribute to open‑source tools developed within the consortium. /li liEngage with the broader research community via the consortium’s network and workshops. /li /ul h3Job requirements /h3 ul liA PhD in computer science, mathematics or a closely related discipline (obtained or expected before the starting date). /li liSolid experience using a proof assistant such as Agda, Rocq or Lean, ideally for non‑trivial formalizations or research on the proof assistant itself. /li liA 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. /li liThe ability to conduct independent research, demonstrated by peer‑reviewed publications at relevant international venues. /li liGood written and spoken English, and the communication skills needed to collaborate effectively within a multi‑site consortium. /li /ul h3Conditions of employment /h3 ul liDuration of contract is 2 years (temporary). /li li36‑40 hours per week. /li liSalary and benefits are in accordance with the Collective Labour Agreement for Dutch Universities. /li liExcellent pension scheme via the ABP. /li liPossibility to compile an individual employment package each year. /li liDiscounts with health insurers on supplemental packages. /li liRegulated leave: 232 leave hours per year (at 38 hours); additional leave can be bought or sold through an individual choice budget. /li liOpportunities for education, training and courses. /li liPartially paid parental leave. /li liAttention to healthy and energetic working life through the vitality program. /li /ul pYour application will receive fair consideration. /p /p #J-18808-Ljbffr
Deel deze vacature: