From Proposition to Program - Embedding the Refinement Calculus in Coq. - Wouter Swierstra; João Alpuim (FLOPS, 2016)

Disjoint intersection types. - Bruno C. d. S. Oliveira; Zhiyuan Shi; João Alpuim (ICFP, 2016)

Disjoint Polymorphism. - João Alpuim; Bruno C. d. S. Oliveira; Zhiyuan Shi (ESOP, 2017)

Embedding the refinement calculus in Coq. - João Alpuim; Wouter Swierstra (Sci. Comput. Program., 2018)