I've just noticed a recent publication:
Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. "On the
expressive power of user-defined effects: effect handlers, monadic
reflection, delimited control." Journal of Functional Programming 29 (2019).
The authors used Abella to formalize several theorems in their paper. Section 7 "Abella Experience Report" is interesting to read.
Best wishes, -Dale