Funded by NWO - Open Competition Domain Science-XL 2023-2024
Duration: June 2025 till June 2030
Web: https://cyclic-structures.gitlab.io/consortium/
Researchers
Project summary
The project aims to improve software reliability by exploring the concept of cyclic structures such as loops in programs, circular communication protocols, and feedback mechanisms in control systems. Cyclic structures come in two forms: some describe processes that eventually stop (inductive structures), while others represent systems designed to run continuously and interact with their environment (coinductive structures). Understanding and verifying these cyclic behaviours is a major challenge in creating reliable software, especially because real-world systems often combine inductive and coinductive structures in complex ways. Current tools and methods are not yet capable of fully analysing such systems, leaving a gap between theoretical models and practical applications. To bridge this gap, they will develop new techniques and tools that unify theory and practice using advanced mathematical principles like coalgebra and coinduction.
The proposed approach covers three facets of the development process for reliable software:
(1) Reliability by Proof - focused on developing foundational methods and tools for cyclic proofs using coalgebraic modal logic to ensure the correctness of systems with cyclic structures;
(2) Reliability by Construction - emphasising the compositional verification of interacting programs based on behavioural type systems and their coalgebraic formulations;
(3) Reliable Proofs by Certification - enhancing proof assistants like Coq and Agda with advanced capabilities for coinductive reasoning, enabling more robust verification of software properties.
This research will push the boundaries of software verification, enhancing areas such as Logic, Programming Languages, Type Theory, Concurrency, and Proof Assistants. Ultimately, it will expand the capabilities of modern tools like Agda and Coq, to verify the behaviour of real-world software written in languages like Rust, paving the way for more reliable and robust systems.
team
Henning Basold (Leiden University)
Georgiana Caltais (University of Twente)
Jesper Cockx (TU Delft)
Helle Hvid Hansen (University of Groningen)
Robbert Krebbers (Radboud University Nijmegen)
Jorge Perez (P.I., University of Groningen)