Adding Equations to System F Types

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

Details

TypeInproceedings
URLhttp://research.microsoft.com/en-us/um/people/nick/feqn.pdf
> Publications > Adding Equations to System F Types