Sep 10, 2025 Our talk proposal “Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning” has bee accepted at IWACO’25. Aug 26, 2025 Our paper “On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs” has bee accepted and will appear at OOPSLA’25. Aug 01, 2025 Our talk proposal “Verifying Effectful Programs via Answer-Type Modification” has bee accepted at OlivierFest 2025. Jun 16, 2025 Our paper “Thrust: A Prophecy-Based Refinement Type System for Rust” has bee accepted and will appear at PLDI’25. Apr 01, 2025 Five internship students, Abhinandan Pal (Obi), Ivana Bocevska, Charlie Walpole, Ate-Jan de Vries, Hanliang Zhang, join our lab. Welcome! Feb 08, 2025 I’m co-chairing the HOPE’25 workshop. Please consider submitting! Jan 01, 2025 Our paper “Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs” has bee accepted and will appear at POPL’25. Dec 31, 2024 This web site has been set up on GitHub Pages.