Type theory, together with the Curry-Howard correspondence is a formal system for stating formal proofs of intuitionistic logic, which is used in constructive mathematics. Intuitionistic logic differs from classical logic in that it doesn’t have the law of excluded middle as a logical axiom/derivation rule. But it does have the principle of explosion: From a proof of False, anything can be derived. Is there a serious attempt to study what can and cannot be proven within mathematics if one takes intuitionistic logic, and drops the axiom that anything can be derived from a proof of False?
Type theory and constructivist mathematics with paraconsistent logic
constructive-mathematicsintuitionistic-logiclogicnonclassical-logictype-theory
Related Solutions
I'm in a hurry but will try to answer a couple of your questions:
Is it correct that the omission of LEM is the distinguishing characteristic of constructive logic as opposed to classical?
Yes!
Is it correct that the Curry-Howard correspondence is conditioned on the omission of LEM?
In a basic version of the Curry–Howard correspondence, you are quite right: There is no program of the type corresponding to LEM. That would be a kind of oracle which is able, for any type $A$, to either produce a value of $A$ or else produce a procedure $A \to \bot$. In particular, with such an oracle there would be an algorithm deciding the halting problem.
Astoundingly, there are more refined versions of the Curry–Howard correspondence which interpret LEM just fine. Every constructive proof gives rise to a pure program while every classical proof gives rise to a program with side effects. Which side effects exactly, depends on the amount of classical axioms used. For interpreting LEM, to have continuations as side effects is enough. For interpreting countable or dependent choice, other side effects are required. You find some references in these slides.
Is it correct that were LEM used in the heart of CoQ and LEAN that in turn these proof checkers would not be proven to halt?
Literally speaking: No. Coq and Lean support LEM just fine as an unproven assumption and still their proof checking terminates.
Is it correct that therefore to conclude that it is LEM that is at the heart of the halting problem?
Yes in some sense and no in some other.
Yes: Without LEM, it becomes possible for all functions $\mathbb{N} \to \mathbb{N}$ to be computable (by a Turing machine or equivalently by an untyped lambda term). The halting function, which maps a number $n$ to $0$ or $1$ depending on whether the $n$-th Turing machine terminates, is no longer a total function $\mathbb{N} \to \mathbb{N}$ in such a world. (Instead, its domain of definition is the subset consisting of those numbers $n$ such that the $n$-th Turing machine terminates or does not terminate.) Accordingly, the question whether there is a Turing machine computing this no-longer-existing gadget loses a bit of its relevance. There are lots of worlds like this, for instance the "effective topos", I tried to give an introduction here.
No: There is a metatheorem stating that every PA-proof of termination of a Turing machine can be mechanically transformed into a HA-proof, and similarly with ZFC and IZF. (PA is Peano Arithmetic, HA is its constructive cousin without LEM; ZFC is Zermelo–Fraenkel set theory with the axiom of choice, IZF is its constructive cousin without LEM and without choice.) So LEM will never be crucial in proving termination of a Turing machine. LEM might be crucial for abstract tools helping with termination proofs, but in the end LEM can always be eliminated from concrete termination results. Keywords to lookup are "Friedman's trick", "continuation trick" or "Barr's theorem".
Best Answer
In general, there are credible early attempts to study aspects of mathematics in the context of paraconsistent calculi (there are many, just look at the ToC of Priest's textbook).
That said, the answer to the precise question you actually asked, the one regarding type theory, is negative.
In type theory (as in most foundational systems), the statement $0=1$ is naturally explosive, in the sense that you can prove anything using $0=1$ without ever invoking $\bot$-elimination. Why? As in my answer to your other question about type theory, given types $A,B$, you can use $\mathbb{N}$-induction to construct a function $f: \mathbb{N} \rightarrow \mathcal{U}$ such that $f(0)$ reduces to $A$ and $f(Sn)$ reduces to $B$. Applying the congruence rule to $0=1$ yields $A = B$, so all types are equal, and in particular $A \rightarrow B$ holds. In fact, Martin-Löf type theory is maximally explosive: if you can inhabit a type $T$ in the empty context without using $\bot$-elimination, an induction on the structure of the proof shows that you could have inhabited the type $T^{\bot \leftarrow 0=1}$, the type obtained from $T$ by replacing every occurrence of $\bot$ with $0=1$. There is nothing specific about $0=1$ here: Martin-Löf type theory without explosion is really just a world where $\bot$ denotes an arbitrary proposition. In particular, if $A$ does not mention $\bot$, then MLTT without explosion proves $A \rightarrow \bot$ precisely if $A$ is explosive.
This means that, as long as you don't intend to add new, classically inadmissible principles, there is not much point in studying these "minimal" type theories based on minimal logic. The situation is more interesting in e.g. the variant of Heyting arithmetic that uses minimal logic instead of intuitionistic logic as its logical substrate. This theory is almost, but not quite, the same as full intuitionistic Heyting arithmetic, since $0=1$ is explosive.
For example, if you want to prove using $0=1$ that every number is even, you can multiply the inconsistent equality by $2$ to get $0=2$, apply transitivity to get $1=2$, then replace $1$ with $2$ in $\forall x. 1x = x$ to conclude $\forall x. 2x=x$, and then $\forall x. \exists y. 2y=x$. You can do this systematically (by induction on the structure of the formula $A$) to prove that $0 = 1 \rightarrow A$.
This time, the converse does not hold, and Heyting arithmetic formulated in minimal logic is not maximally explosive: there are positive statements that it proves false, but that are not explosive. That's because one of the axioms of Heyting arithmetic says something non-trivial about $\bot$. There are two ways to conclude $\bot$ in Heyting arithmetic:
From an induction axiom. This is not a problem: when you replace all occurrences of $\bot$ with $0=1$ in an induction axiom, the result is another induction axiom. (This is the only case in MLTT, which is why it justifies explosion.)
By applying the non-logical axiom $\forall x. 0 = Sx \rightarrow \bot$ to some $St = 0$. The problem is that you cannot replace this axiom with $\forall x. 0 = Sx \rightarrow 0 = 1$: it takes some work to show that this really cannot be done: it turns out that $0 = 2$ does not provably imply $0=1$ if you formulate Heyting arithmetic inside minimal logic. For details you can consult Heerkens' MSc thesis.
This is, however, the only obstacle: you replace $\forall x. 0 = Sx \rightarrow \bot$ with $\forall x. 0 = Sx \rightarrow 0 = 1$, and you get a minimal arithmetic that coincides perfectly with intuitionistic Heyting arithmetic. One can argue that this modified axiom is philosophically justified purely on basis of what we want arithmetic to be.