Effectful Realizability: Frameworks and Applications, ISF, 2025--2010 [abstract]
Coinduction in Lean: Certified Circular Reasoning (with Alexandra Silva), BSF, 2025--2029 [abstract]
Extending and Applying Implemented Intuitionistic Mathematics (with Robert Constable), BSF, 2021--2025 [abstract]
 
- Recipient of the Pazy Memorial Research Award
Formalizing Coinduction via Closure Operators and Proof Cycles, ISF, 2021--2025 [abstract]
Real-time Risk Assessment in Machine-Learning-based Autonomous Systems , BGU Data Science Research Grant, 2022
Cyclic Reasoning Mechanisms for Interactive Theorem Proving, The Royal Society, 2021--2022
Real-time Robustness Proving in Machine Learning Models , BGU Data Science Research Grant, 2020