Simple example for Higher Order Abstract Syntax (λ-tree syntax)
Well, this is a bit broad but the basic idea is the following. In First-order abstract syntax (FOAS) we model lambda terms following their syntax tree. E.g., in Coq we would write

(* FOAS *)
Definition variable := string .
Inductive term: Set :=
  | var: variable -&gt; term
  | app: term -&gt; term -&gt; term
  | lam: variable -&gt; term -&gt; term
.

Definition example: term := lam "x" (app (var "x") (var "x")) .


Note how we model $\lambda x. xx$ by storing the name "x" explicitly.
In a sense, a lambda is represented as a pair (variable name, body).

In FOAS we need to carefully handle alpha-conversion and capture-avoiding substitutions.

In HOAS, we model lambdas as functions, not pairs, exploiting the functions in the host language.

(* HOAS *)
Inductive term: Set :=
  | var: variable -&gt; term    (* vars are usually removed in HOAS *)
  | app: term -&gt; term -&gt; term
  | lam: (term -&gt; term) -&gt; term

Definition example: term = lam (fun x: term =&gt; app x x) .


(Note that this won't type check in Coq since it does not use positive recursion, as Mario Carneiro points out below. Still, you get the idea.)

No need to handle alpha-conversion (or substitutions) here since the name "x" is no longer stored in the term.

What we lose in HOAS is the ability to dissect the term representation (e.g. structural induction on the syntax tree) as easily as we could in FOAS.