Lambda the Ultimate

The ongoing thread On the (Alleged) Value of Proof for Assurance has sparked a discussion about applying the Curry Howard Isomorphism to more than intuitionistic logic and the simply typed LC. All these attempts are rather hand-wavey to me, but the discussion revolves around Isabelle and Coq, neither of which do I know.

Neelk has made it pretty clear that CH does not apply to Isabelle, but it has gotten me wondering.

* Is there a rigorous way to apply CH to a more powerful type system than the simply typed LC?

* Is it nonsensical to try and apply it?

* Does the ability to type-check non-terminating expressions have an impact? Similarly, do existential types? (I'm thinking F-Omega)

* Are there any articles/books that do apply it to more powerful type systems which are accessible to someone without a PhD?