Adding Equations to System F Types

Neelakantan Krishnaswami and Nick Benton

Abstract

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.

Details

Publication typeInproceedings
Published inProceedings of the 22nd European Symposium on Programming (ESOP 2012). March 2012
URLhttp://research.microsoft.com/en-us/um/people/nick/feqn.pdf
PublisherSpringer Verlag
> Publications > Adding Equations to System F Types