Safety Analysis versus Type Inference for Partial Types

Abstract

Safety analysis is an algorithm for determining if a terin in an untyped lambda calculus with constants is safe, i.e., if it does not cause an error during evaluation. We prove that safety analysis accepts strictly more safe lambda terms than does type inference for Thatte's partial types.