(*<*)
theory Paper
imports "../Nominal/Test"
begin
(*>*)

section {* Introduction *}

text {*

  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, Spi-calculus

  Contributions:  We provide definitions for when terms
  involving general bindings are alpha-equivelent.
*}

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

section {* Abstractions *}

section {* 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.


*}



(*<*)
end
(*>*)