The Curry-Howard Correspondence is about proof systems. You would have a very hard time finding a proof theorist that says it's okay to have an undecidable proof checker or an inconsistent one.
For that reason, only _typed_ lambda calculi have any hope of corresponding to a proof system. You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent.
Perhaps a para-consistent logic might work, but we're getting very exotic here.
For that reason, only _typed_ lambda calculi have any hope of corresponding to a proof system. You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent.
Perhaps a para-consistent logic might work, but we're getting very exotic here.