Completeness and Cut-elimination in the Intuitionistic Theory of Types. - Mary DeMarco; James Lipton (J. Log. Comput., 2005)

Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog. - Gianluca Amato; Mary DeMarco; James Lipton (CoRR, 2024)