As Zhen Lin has mentioned in the comments, the specifics will depend on how you are interpreting $=$ in your type theory. Here I will outline how $=$ is handled in
HoTT for concreteness, but you will see that once we have a fixed type representing equality, everything works how you would expect.
In HoTT, we add the following inference rule to our logic:
$$\frac{\Gamma \vdash A \text{ type} \quad \Gamma \vdash a, b : A}{\Gamma \vdash a =_A b \text{ type}}$$
That is, for every type $A$, and for every two values $a,b : A$, we assert the existence of a type $a =_A b$. Values inhabiting this type are proofs that $a$ and $b$ are equal.
To talk about how values $p : a =_A b$ are programs, we will talk about their introduction/elimination rules. I'm going to play slightly fast and loose with my notation here to try and keep the rules legible. If you want the gory details, see the appendix in the HoTT book linked above.
There is only one introduction rule:
$$ \frac{\Gamma \vdash A \text{ type} \quad \Gamma \vdash a : A}{\Gamma \vdash \text{refl}_a : a =_A a}$$
There is always a proof $\text{refl}_a$ (for reflexivity) asserting that $a=a$.
The elimination rule is rather subtle. It forms the basis of what is called "path induction" in HoTT, and is a common source of confusion when getting started. I won't go into too much detail about these subtleties here, though.
$$
\frac{
\Gamma, p:a =_A b \vdash C(p) \text{ type}
\quad
\Gamma, a_0 : A \vdash c(a_0) : C(\text{refl}_{a_0})
}{
\Gamma \vdash \text{ind}_{=_A}(c) : C(p)
}
$$
This says that given any type family $C$ depending on $p : a =_A b$, if we can eliminate the only introduction rule, then we can eliminate the entire type. That is, if some $c(a_0) : C(\text{refl}_{a_0})$, then we can get a value $\text{ind}_{=_A}(c) : C(p)$ for any $p : a =_A b$ we like. Moreover, $\text{ind}_{=_A}$ satisfies the computation rule:
$$(\text{ind}_{=_A}(c))(\text{refl}_a) = c(a)$$
If it seems surprising to you that we get all of this expressivity by working only with $\text{refl}_a$, you're in good company. This is just the tip of the "subtlety" iceberg that I was referring to earlier. Intuitively, since $\text{refl}_a$ is the only constructor for an equality type, once we prove something for it, we've proven something for the whole equality type. This is analogous to proving something for every value in $\mathbf{1}$ by proving it for $\ast : \mathbf{1}$. The only difference is in our heads: We like to imagine $\ast$ as being the only element of $\mathbf{1}$, while it's easy for us to imagine multiple possible elements of $a =_A b$, especially since our only constructor is for $a =_A a$, which feels like a weaker condition.
Of course, type theory doesn't care about our hang-ups. There are plenty of models of type theory with equality where $\text{refl}_a$ honestly is the only value of any equality type.
As for actually "computing" things with equality types, the obvious practicality of the rest of the lambda calculus breaks down somewhat. While we are technically programming, I'm not sure if there's any analogue of equality types that, say, a software engineer might care about. This is in stark contrast to other constructions in type theory, which correspond to algebraic datatypes (and which thus have obvious real-world computational applications we can point to). I'm sure somebody has thought of what these types can properly compute, but I'm not familiar with any literature on the subject.
I hope this helps ^_^
