Give an example of a program in Simply Typed Lambda that produces Bottom. I'm not sure how bottom applies to simply typed lambda calculus.
not A is a common abbreviation for A -> ⊥
But I see no way to construct a function of that signature within the theory.
Edit: A more precise way of phrasing my original question is "Is it impossible to prove a negation (A -> ⊥) unless another negation is specified?"
Since if you are given a constant t1:A->⊥ and if you are given the constant t2:B->A then it is trivial to construct a function to Bottom (t1 t2):B->⊥.
If no constant that returns bottom is provided, bottom can never be can never be proven in Simply Typed Lambda Calculus?
Thanks
 A: Simply typed lambda calculus is strongly normalizing (Intensional Interpretations of Functionals of Finite Type I, W.W. Tait, JSL 32(2), 1967).
Given a base type $A \ne \bot$, if there was a term of type $\neg A$, then its normal form (which exists as we've just seen) would be of the form $\lambda x:A. M$, with $x:A \vdash M : \bot$. Since $M$ is a normal form, it must be either of the form $x N$ (impossible because $x$ does not have a function type) or $\lambda y:B. N'$ (impossible because $M$ does not have a function type). So there is no such term.
There can of course be functions whose return type is $\bot$, if the argument lets $\bot$ in. For example there is an obvious function of type $\bot\rightarrow\bot$.
This is a general phenomenon: in a typed lambda calculus which is strongly normalizing, there is no way to construct a term of type $\bot$, short of introducing ad hoc constants. In the Curry-Howard correspondence, $\bot$ is the type of false propositions. Strongly normalizing calculi do not allow proving false propositions, so they have no closed term of type $\bot$.
Lambda calculus with intersection types is an interesting extension. This calculus defines all terms to have the type $\top$, and has the properties that a term can be typed without using $\top$ if and only if it has a normal form. This gives a simple type-theoretic characterization of terminating computations (of course, typing is not decidable).
See Does there exist a Turing complete typed lambda calculus?
A: There is no equivalent to  negation or absurdity in simply typed lambda calculus as it only corresponds to the implicational fragment of propositional intuitionistic logic. However, the map from a type to its inhabitant does seems to be a good way to represent absurdity as shown here, but this can only be constructed with polymorphism. Also, note that this only gives an uninhabited type if the context has uninhabited types. On the other hand there is the trivial situation where every type is inhabited in the context (corresponding to the situation of only considering true propositions). However, another unoccupied type/negation need not be specified, it just has to exist.
