Publications

Certified Compilers à la Carte
O. Ebresafe, I. Zhao, E. Jin, A. Bright, C. Jian, Y. Zhang
PLDI, 2025
[ paper | technical report | implementation ]
Adds nested families to Family Polymorphism. This paradigm can scale.

Extensible Metatheory Mechanization via Family Polymorphism
E. Jin, N. Amin, Y. Zhang
PLDI, 2023
[ paper | technical report | implementation ]
Compiles Family Polymorphism to Rocq modules and functors. Addresses the expression problem in proof engineering.

Universal Quantification and Implication in miniKanren
E. Jin, G. Rosenblatt, M. Might, L. Zhang
Relational Programming Workshop, 2021
[ paper ]
Attempts to lift miniKanren to FOL.