It has not yet fared so well in the POPLmark challenge

  as the second part contain a formalisation of records 

  where ...

  The difficulty can be appreciated by considering that the

  definition given by Leroy in [] is incorrect (it omits a

  side-condition).

  Examples: type-schemes

  Contributions:  We provide definitions for when terms

  involving general bindings are alpha-equivelent.

*}

text {* A Brief Overview about the Nominal Logic Work *}

text {* Abstractions *}

text {* Alpha-Equivalence and Free Variables *}

text {*

  Acknowledgements: We thank Andrew Pitts for the many discussions

  about the topic. We thank Peter Sewell for making [] available 

  to us and explaining some of the finer points of the OTT tool.