What is a constructive proof of $\lnot\lnot(P\vee\lnot P)$?

Per the BHK interpetation, a proof of $(P \lor (P \to \bot)) \to \bot$ is pair of procedures, one for each disjunct in the hypothesis.

• The first, $s_1$, is a procedure which takes a proof of $P$ as input and produces a proof of $\bot$. In other words, the first is a proof of $P \to \bot$.

• The second, $s_2$, takes any proof of $P \to \bot$ as input and produces a proof of $\bot$. In other words, it is a proof of $(P \to \bot) \to \bot$.

By composing these to form $s_2(s_1)$, we obtain a procedure which takes no input and produces a proof of $\bot$.

The procedure just described (composition) takes any proof of $(P \lor (P \to \bot)) \to \bot$ and produces a proof of $\bot$. This means that $((P \lor (P \to \bot))\to \bot) \to \bot$ is provable.

This description shows how to write a $\lambda$ expression of the appropriate type. All that it does is to break the input into its two components and run the second one with the first as input. In particular, if we view $(P \lor \lnot P) \to \bot$ as a type $p(n,s)$ such that $\lambda s.p(1,s)$ is of type $P \to \bot$ and $\lambda\,s.p(2,s)$ is of type $\lnot P \to \bot$ then $$\lambda\, p(n,s) . p(2,\lambda\, s.p(1,s))$$ is of type $((P \lor \lnot P) \to \bot) \to \bot$

Here's a natural deduction proof:

1. $\lnot (P \lor \lnot P)$ [Assumption]
2. $\lnot P \land \lnot \lnot P$ [De Morgan]
3. $\lnot P$ [$\land$ elimination]
4. $\lnot \lnot P$ [$\land$ elimination]
5. $\bot$ [$\bot$ introduction from 3., 4.]
6. $\lnot \lnot (P \lor \lnot P)$ [$\lnot$ introduction]

Although I've already accepted Carl Mummert's answer, which was just what I wanted, I'm going to append the following variations for future reference.

First, a proof:

1: Assume $((a\vee(a\to\bot))\to\bot$
2a: Assume $a$
2b: $a\vee(a\to\bot)$ [2a, right $\vee$]
2c: $\bot$ [1, 2b, mp]
3: $a\to\bot$ [2a–2c]
4: $a\vee(a\to\bot)$ [3, left $\vee$]
5: $\bot$ [1, 4, mp]
6: $(((a\vee(a\to\bot))\to\bot)\to\bot$ [1–5]

And a program with the requisite type:

λf.
  let g = λa. f (Left a)
  let h = λn. f (Right n)
in
  h g

a has type $a$,
n and g have type $a\to\bot$,
f has type $(((a\vee(a\to\bot))\to\bot)$, and
h has type $((a\to\bot)\to\bot)$.

Finally, the Haskell term

\f -> let   
        g = \a -> f (Left a)
        h = \n -> f (Right n)
        in h g

is accepted by GHC and has type (Either a (a -> t) -> t) -> t.
We can β-reduce this term to

\f -> f (Right ( \a -> f (Left a) ))

which has the same type.