Sorry, by "untyped" I meant "dynamically typed." CL does have a sophisticated type hierarchy, but to my knowledge, according to the standard, types are checked

Sorry, by "untyped" I meant "dynamically typed." CL does have a sophisticated type hierarchy, but to my knowledge, according to the standard, types are checked at runtime, right? In the type-theoretic sense, "type" refers to a statically known classification. Curry-Howard is the idea that static types are propositional formulas and expressions that have such types are their proofs. Under the Curry-Howard correspondence, a static typechecker analyzing your program is equivalent to a proof checker ensuring that your proof is valid. People tend to invoke Curry-Howard to praise ML- and Haskell-style algebraic types (according to Curry-Howard, sum types are disjunction, product types are conjunction, and function/exponential types are implication).