I would like some help choosing the rules for the empty type. I am trying to setup a typed lambda calculus with sums like in
Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums
Except, I am being explicit about type formation (that is, I am keeping track of a context, and applying rules to form types, in a similar way to page 554 of the homotopy type theory book). For example, here is one of my introduction rules for sum types:
$$\begin{array}{c} \Gamma\vdash x:A\hspace{1em}\Gamma\vdash B:\text{type}\\ \overline{\Gamma\vdash\text{inl}_{A+B}(x):A+B} \end{array}$$
My questions are (1) whether the following is appropriate for being an elimination rule for the empty type:
$$\begin{array}{c} \underline{\Gamma\vdash A:\text{type}\hspace{1em}\Gamma\vdash e:0}\\ \Gamma\vdash\text{abort}_{A}(e):A \end{array}$$
And (2) whether the following is appropriate for being a computation rule for the empty type:
$$\begin{array}{c} \Gamma,e:0\vdash x:A\\ \overline{\Gamma,e:0\vdash\text{abort}_{A}(e)=x:A} \end{array}$$
And if not, then what rules should I use ? I do not think my situation is helped by the fact that I do not understand the equational rule for the empty type in the above reference.
Your elimination rule is correct. In a simple type theory (i.e. without dependent types), you could write the computation rule for the empty type as the following (note that this matches the rule in the paper you link, though the notation is a little different, and I've been explicit about the type $A$). $$\frac{\Gamma \vdash e : 0 \qquad \vdash A\ \mathrm{type} \qquad \Gamma \vdash a : A}{\Gamma \vdash \mathrm{abort}_A(e) \equiv a : A}$$ You will usually not have contexts of the form $\Gamma, x : A$ (or $\Gamma, e : 0$) in a simple type theory unless you're describing a variable-binding operator (like $\lambda$-abstraction). In the HoTT book, there are more rules of this form because they have dependent types (where you have to take more care about variable binding).