Verifying and Synthesizing Constant-Resource Implementations with Types

Van Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson +1

We propose a novel type system for verifying that programs correctly implement constant-resource behavior. Our type system extends recent work on automatic amortized resource analy…