π-calculus, Session Types research at the University of Oxford
Subject Reduction and Progress for Synchronous Multiparty Session Types in Rocq.