10   Here can come any text.

    10 

    11   It has not yet fared so well in the POPLmark challenge

    12   as the second part contain a formalisation of records 

    13   where ...

    14 

    15   The difficulty can be appreciated by considering that the

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

    17   side-condition).

    18 

    19   Examples: type-schemes

    20 

    21   Contributions:  We provide definitions for when terms

    22   involving general bindings are alpha-equivelent.

    23 *}

    24 

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

    26 

    27 text {* Abstractions *}

    28 

    29 text {* Alpha-Equivalence and Free Variables *}

    30 

    31 

    32 text {*

    33   Acknowledgements: We thank Andrew Pitts for the many discussions

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

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

    36