397 early-career researchers have won a European Research Council (ERC) Starting Grants. Following the first call for proposals under the EU’s new R&I programme, Horizon Europe, €619 million will be invested in excellent projects dreamed up by scientists and scholars.

The researcher of the IMDEA Software Institute, Niki Vazou, has been awarded an ERC Starting Grant worth €1.5 million, for the project “Certified Refinement Types”. It will help her to launch their own project, form a team and pursue her best ideas.

The CRETE project

Refinement types are a promising verification technology that in the last decade has spread to mainstream languages (e.g., Haskell, C, Ruby, Scala, and the ML-family) to verify sophisticated properties of real world applications, e.g., safety of cryptographic protocols, memory and resource usage, and web security.

The weakness of refinement types is that they do not meet the soundness standards set by theorem provers. A sound verification system accepts as safe only those programs that never violate their specifications. Refinement type checkers (e.g., Liquid Haskell, F*, and Stainless) approximately report five unsoundness bugs per year, as opposed to only one reported by the Coq theorem prover. This rarity of unsoundness bugs in Coq is unsurprising since Coq is designed to soundly machine check mathematical proofs. Coq’s soundness design recipe though cannot be directly applied to refinement type checkers that aim to practically verify real world programs.

The goal of CRETE is to design a sound and practical refinement type system. This is an ambitious goal that entails the development of a verification system that is as practical as refinement types and constructs machine-checked mathematical proofs. The system will be implemented on refinement type systems for mainstream languages (i.e., Haskell and Rust) and will be evaluated on real-world code, such as web applications and cryptographic protocols.

“Funded by the European Union. Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.” Ref.: 101039196.