VeriML: typed computation of logical terms inside a language with effects. - Antonis Stampoulis; Zhong Shao 001 (ICFP, 2010)

Static and user-extensible proof checking. - Antonis Stampoulis; Zhong Shao 001 (POPL, 2012)

Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam. - Antonis Stampoulis; Adam Chlipala (Proc. ACM Program. Lang., 2018)