Contextual equivalence for inductive definitions with binders in higher order typed functional programming

Matthew R. Lakin, Andrew M. Pitts. Contextual equivalence for inductive definitions with binders in higher order typed functional programming. Journal of Functional Programming, 23(6):658-700, 2013. [doi]

Abstract

Abstract is missing.