Neelakantan Krishnaswami and Nick Benton
We present an extension of System F with types for termlevel equations. This internalization of the rich equational theory of the polymorphic lambda calculus yields an expressive core language, suitable for formalizing features such as Haskell's rewriting rules mechanism or Extended ML signatures.
In Proceedings of the 22nd European Symposium on Programming (ESOP 2012). March 2012
Publisher Springer Verlag