JOBDESCRIPTION

Essential to writing and reasoning about software that operates continuously is a practically usable language for programs and proofs of coinductive types. Proof assistants currently rely on either syntactic guardedness conditions on programs, sized types, or guarded recursion. However, the syntactic guardedness condition is very restrictive and brittle, while both sized types and guarded recursion require significant additional annotations to the program.
As a PhD student in this project, you will work towards developing a new system for defining and reasoning about coinductive processes in proof assistants. The key challenge is to develop a system that is both modular (so productivity information is propagated through the type system) and user-friendly (so few or no manual annotations are needed).

This project combines and builds on existing approaches proposed in the literature:

• Sized types and guarded type theory, in particular their implementation in Agda (see A. Abel and B. Pientka: “Wellfounded recursion with copatterns: a unified approach to termination and productivity”, ICFP’13).
• Coinductive reasoning in (higher) observational type theory and cubical type theory (see R. Atkey and C. McBride: “Productive coprogramming with guarded recursion”, ICFP’13).

In order to ensure soundness and usability, this project will require a combination of theoretical analysis of a type theory with first-class reasoning about coinductive processes and the development of a prototype implementation of this type theory as an extension to Agda.
This PhD position is part of the NWO XL project “Cyclic Structures in Programs and Proofs”, which has positions in Groningen, Leiden, Twente, and Nijmegen. As a PhD student in this project, you will collaborate with other researchers working within this project by attending the NetTCS workshop (https://nettcs.cs.ru.nl/) and through individual collaborations.For other vacancies: https://cyclic-structures.gitlab.io/vacancies/

JOB REQUIREMENTS

We seek strong, highly motivated applicants who:

• Have (or are close to completing) an MSc in Computer Science, Logic, Mathematics, or a related field.
• Have background or research experience in any of the areas above (preferred but not required).
• Have strong communication skills (oral and written) in English.

Please refer the Job description for details