Simon Ambler, Roy L. Crole, Alberto Momigliano. Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction. In Victor Carreño, César Muñoz, Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings. Volume 2410 of Lecture Notes in Computer Science, pages 13-30, Springer, 2002. [doi]
Abstract is missing.