A Logic for Reasoning with Higher-Order Abstract Syntax. - Raymond McDowell; Dale Miller 001 (LICS, 1997)

Cut-elimination for a logic with definitions and induction. - Raymond McDowell; Dale Miller 001 (Theor. Comput. Sci., 2000)

Reasoning with higher-order abstract syntax in a logical framework. - Raymond McDowell; Dale Miller 001 (ACM Trans. Comput. Log., 2002)

Encoding transition systems in sequent calculus. - Raymond McDowell; Dale Miller 001; Catuscia Palamidessi (Theor. Comput. Sci., 2003)