Exceptions Are Strictly More Powerful Than Call/CC.

Also appears as Fox Memorandum CMU-CS-FOX-95-03. We demonstrate that in the context of statically typed pure functional lambda calculi, exceptions are strictly more powerful than call/cc. More precisely, we prove that the simply typed lambda calculus extended with exceptions is strictly more powerful than Girard's F [6, 15] (a superset of the simply typed lambda calculus) extended with call/cc and abort. This result is established by showing that the rst language is Turing equivalent while the second language permits only a subset of the recursive functions to be written. We show that the simply typed lambda calculus extended with exceptions is Turing equivalent by reducing the untyped lambda calculus to it by means of a novel method for simulating recursive types using exception-returning functions. The result concerning F extended with call/cc is from a previous paper of the author and Robert