Matthew R. Lakin, Andrew M. Pitts: Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming. ESOP 2009: 47-61