A Verified Cost Model for Call-By-Push-Value. - Zhuo Zoey Chen; Johannes Åman Pohjola; Christine Rizkallah (ITP, 2025)

cbpv-reasonable-HOL. - Zhuo Zoey Chen; Johannes Åman Pohjola; Christine Rizkallah (DROPS Artifacts, 2025)