Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Adding Equations to System F Types

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.


Publication typeInproceedings
Published inProceedings of the 22nd European Symposium on Programming (ESOP 2012). March 2012
PublisherSpringer Verlag
> Publications > Adding Equations to System F Types