In this paper, we model fresh names in the $\pi$-calculus using
  \emph{abstractions} w.r.t. a new binding operator $\theta$.  Both
  the theory and the metatheory of the $\pi$-calculus benefit from
  this simple extension.  The operational semantics of this new
  calculus is \emph{finitely branching}. Bisimulation can be given
  without mentioning any constraint on names, thus allowing for a
  straightforward definition of a \emph{coalgebraic} semantics. This
  is cast within a category of coalgebras over algebras with
  infinitely many unary operators, in order to capitalize on $\theta$.
  Following previous work by Montanari and Pistore, we present also a
  \emph{finite} representation for \emph{finitary} processes and a
  finite state verification procedure for bisimilarity, based on the
  new notion of \emph{$\theta$-automaton}.  Finally, we improve
  previous encodings of the $\pi$-calculus in the Calculus of
  Inductive Constructions.