Algorithm for deciding alpha-equivalence of terms in languages with bindings

Question

I am interested in the alpha equivalence relation in languages with variable bindings, such as:

t := x:y    'x belong to y'
  | bot     'False'
  | t -> t  'implication'
  | Ax.t    'forall x, t'

Or the pure lambda calculus:

t := x       'variable'
  | (t t)    'application '
  | Lx.t     'abstraction: \x -> t'

I am looking for an algorithm allowing me to determine whether two terms of the language are alpha-equivalent or not. Any published reference is very welcome too. I am assuming a data representation of the terms as a standard recursive type, for example in Haskell:

newtype Var = Var Int 
data Term = Belong Var Var
          | Bot
          | Imply Term Term
          | Forall Var Term